Grace/Cumulus/Real/Analysis/HeineCantor.g17

Open in Workbench Download source

Imports

Set.Choice · ExtremeValue

Declarations

Source

1-- Real analysis: HeineCantor2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Real.Analysis.HeineCantor8import Set.Choice9import ExtremeValue1011-- Section: UniformFirstWitnessGraph12defchoose failureFirst (f S : Set, E : Real, n : Nat) (X ∈ ℝ) :=13  ∃ Y ∈ ℝ, UniformFailurePair(f, S, E, dyadicRadius(n), X, Y)14requires witnesses : ∀ D ∈ ℝ, (0 < D →15  ∃ X ∈ ℝ, ∃ Y ∈ ℝ, UniformFailurePair(f, S, E, D, X, Y))16proof17  have radiusReal := dyadicRadius.real at n with assumption18  have radiusMember : dyadicRadius(n) ∈ ℝ19    unfold Real at radiusReal20    exact radiusReal21  have positive := dyadicRadius.positive at n with assumption22  exact witnesses with dyadicRadius(n), radiusMember, positive2324defchoose failureSecond (f S : Set, E : Real, n : Nat) (Y ∈ ℝ) :=25  UniformFailurePair(f, S, E, dyadicRadius(n), failureFirst(f, S, E, n), Y)26requires witnesses : ∀ D ∈ ℝ, (0 < D →27  ∃ X ∈ ℝ, ∃ Y ∈ ℝ, UniformFailurePair(f, S, E, D, X, Y))28proof29  obtain ⟨firstReal, Y, realY, bad⟩ :=30    failureFirst.selected at f, S, E, n with witnesses31  witness Y32  refine ⟨realY, bad⟩3334-- UniformChoicePair35theorem failureWitnesses.pair (f S : Set, E : Real, n : Nat)36  requires witnesses : ∀ D ∈ ℝ, (0 < D →37    ∃ X ∈ ℝ, ∃ Y ∈ ℝ, UniformFailurePair(f, S, E, D, X, Y))38  shows failureFirst(f, S, E, n) ∈ ℝ ∧39    failureSecond(f, S, E, n) ∈ ℝ ∧40    UniformFailurePair(f, S, E, dyadicRadius(n),41      failureFirst(f, S, E, n), failureSecond(f, S, E, n))42proof43  have first := failureFirst.selected with witnesses44  have second := failureSecond.selected with witnesses45  rcases first with ⟨firstReal, availableSecond⟩46  rcases second with ⟨secondReal, bad⟩47  refine ⟨firstReal, secondReal, bad⟩4849-- UniformChoice50defgraph failureFirstSequence (f S : Set, E : Real) (n ∈ ℕ) : ℝ :=51  failureFirst(f, S, E, n)52requires witnesses : ∀ D ∈ ℝ, (0 < D →53  ∃ X ∈ ℝ, ∃ Y ∈ ℝ, UniformFailurePair(f, S, E, D, X, Y))54proof55  obtain ⟨realFirst, realSecond, bad⟩ := failureWitnesses.pair with witnesses56  exact realFirst5758defgraph failureSecondSequence (f S : Set, E : Real) (n ∈ ℕ) : ℝ :=59  failureSecond(f, S, E, n)60requires witnesses : ∀ D ∈ ℝ, (0 < D →61  ∃ X ∈ ℝ, ∃ Y ∈ ℝ, UniformFailurePair(f, S, E, D, X, Y))62proof63  obtain ⟨realFirst, realSecond, bad⟩ := failureWitnesses.pair with witnesses64  exact realSecond6566-- UniformFirstWitnessGraph67theorem failureFirstSequence.sequence (f S : Set, E : Real)68  requires witnesses : ∀ D ∈ ℝ, (0 < D →69    ∃ X ∈ ℝ, ∃ Y ∈ ℝ, UniformFailurePair(f, S, E, D, X, Y))70  shows RealSequence(failureFirstSequence(f, S, E))71proof72  unfold RealSequence73  exact failureFirstSequence.function with witnesses7475-- Section: HeineCantor76theorem failureSecondSequence.sequence (f S : Set, E : Real)77  requires witnesses : ∀ D ∈ ℝ, (0 < D →78    ∃ X ∈ ℝ, ∃ Y ∈ ℝ, UniformFailurePair(f, S, E, D, X, Y))79  shows RealSequence(failureSecondSequence(f, S, E))80proof81  unfold RealSequence82  exact failureSecondSequence.function with witnesses8384-- UniformWitnesses85theorem failureWitnesses.properties (f S : Set, E : Real)86  requires witnesses : ∀ D ∈ ℝ, (0 < D →87    ∃ X ∈ ℝ, ∃ Y ∈ ℝ, UniformFailurePair(f, S, E, D, X, Y))88  shows TermsIn(failureFirstSequence(f, S, E), S) ∧89    TermsIn(failureSecondSequence(f, S, E), S) ∧90    AsymptoticallyClose(failureSecondSequence(f, S, E),91      failureFirstSequence(f, S, E)) ∧92    (∀ n ∈ ℕ, ¬(f(failureFirstSequence(f, S, E)[n]) ∈93      openBall(f(failureSecondSequence(f, S, E)[n]), E)))94proof95  constructor96    intros n naturalN97    have typedN : Nat(n) by exact nat.omega.backward at n with naturalN98    obtain ⟨realFirst, realSecond, bad⟩ := failureWitnesses.pair with witnesses99    rcases bad with ⟨memberFirst, memberSecond, near, far⟩100    have value := failureFirstSequence.value with witnesses101    rwa value102  . constructor103      intros n naturalN104      have typedN : Nat(n) by exact nat.omega.backward at n with naturalN105      obtain ⟨realFirst, realSecond, bad⟩ := failureWitnesses.pair with witnesses106      rcases bad with ⟨memberFirst, memberSecond, near, far⟩107      have value := failureSecondSequence.value with witnesses108      rwa value109    . constructor110        constructor111        . exact failureSecondSequence.sequence with witnesses112        . constructor113          . exact failureFirstSequence.sequence with witnesses114          . intros D realD positiveD115            obtain ⟨N, naturalN, small⟩ := dyadicRadii.eventually_below with positiveD116            witness N117            constructor118            . exact naturalN119            . intros n indexNatural afterN120              obtain ⟨realFirst, realSecond, bad⟩ :=121                failureWitnesses.pair at f, S, E, n with witnesses122              rcases bad with ⟨memberFirst, memberSecond, near, far⟩123              have radiusSmall := small with n, indexNatural, afterN124              have weak := realLess.implies_le with radiusSmall125              have enlarged := openBall.mono with near, weak126              have firstValue := failureFirstSequence.value at127                f, S, E, n with witnesses128              have secondValue := failureSecondSequence.value at129                f, S, E, n with witnesses130              rwa [firstValue, secondValue]131      . intros n naturalN132        obtain ⟨realFirst, realSecond, bad⟩ :=133          failureWitnesses.pair at f, S, E, n with witnesses134        rcases bad with ⟨memberFirst, memberSecond, near, far⟩135        have firstValue := failureFirstSequence.value at136          f, S, E, n with witnesses137        have secondValue := failureSecondSequence.value at138          f, S, E, n with witnesses139        rwa [firstValue, secondValue]140141-- CompactUniformContinuity142theorem ContinuousOn.uniform_of_sequentially_compact (f S : Set)143  requires continuous : ContinuousOn(f, S)144  requires compact : SequentiallyCompact(S)145  shows UniformContinuousOn(f, S)146proof147  by_contra notUniform148  obtain ⟨E, realE, positiveE, witnesses⟩ := ContinuousOn.nonuniform_pairs with continuous, notUniform149  obtain ⟨termsFirst, termsSecond, close, far⟩ := failureWitnesses.properties with witnesses150  have sequenceSecond := failureSecondSequence.sequence with witnesses151  obtain ⟨k, increasing, L, realL, memberL, mapsSecond, mapsFirst⟩ := ContinuousOn.nearby_compact_images with152    continuous, compact, sequenceSecond, termsSecond, termsFirst, close153  have function : f : ℝ → ℝ154    rcases continuous with ⟨function, subset, atPoints⟩155    exact function156  obtain ⟨N, naturalN, near⟩ := ConvergesTo.eventually_near_each_other with mapsSecond, mapsFirst, positiveE157  have typedN : Nat(N) by exact nat.omega.backward at N with naturalN158  have afterN := LessEqual.reflexive with typedN159  have selectedNear := near with N, naturalN, afterN160  have selectedSecondSequence := subsequence.sequence with sequenceSecond, increasing161  have sequenceFirst := failureFirstSequence.sequence with witnesses162  have selectedFirstSequence := subsequence.sequence with sequenceFirst, increasing163  have mappedSecond := compose.apply at164    f, subsequence(failureSecondSequence(f, S, E), k), ℕ, ℝ, ℝ, N with165      selectedSecondSequence, function, naturalN166  have mappedFirst := compose.apply at167    f, subsequence(failureFirstSequence(f, S, E), k), ℕ, ℝ, ℝ, N with168      selectedFirstSequence, function, naturalN169  rw [mappedFirst, mappedSecond] at selectedNear170  have chosenSecond := subsequence.value with sequenceSecond, increasing171  have chosenFirst := subsequence.value with sequenceFirst, increasing172  rw [chosenFirst, chosenSecond] at selectedNear173  have selectorFunction := StrictlyIncreasingNat.function with increasing174  have selectedNatural := FunctionBetween.apply_closed with selectorFunction, naturalN175  have contradiction := far with k[N], selectedNatural176  exact contradiction with selectedNear177178-- HeineCantor179theorem closedInterval.heine_cantor (f : Set, A B : Real)180  requires continuous : ContinuousOn(f, closedInterval(A, B))181  shows UniformContinuousOn(f, closedInterval(A, B))182proof183  have compact := closedInterval.sequentially_compact at A, B with184    *{2}185  exact ContinuousOn.uniform_of_sequentially_compact with continuous, compact186187-- Section: DomainSequentialContinuity188predicate RealFunctionOn (f S : Set) :=189  ∃ D, D ⊆ ℝ ∧ S ⊆ D ∧ FunctionBetween(f, D, ℝ)190191predicate ContinuousWithinDomainAt (f S : Set) (A : Real) :=192  RealFunctionOn(f, S) ∧ S ⊆ ℝ ∧ A ∈ S ∧193  (∀ E ∈ ℝ, 0 < E →194    ∃ D ∈ ℝ, 0 < D ∧195      ∀ X ∈ ℝ, (X ∈ S → (X ∈ openBall(A, D) →196        f(X) ∈ openBall(f(A), E))))197198predicate ContinuousOnDomain (f S : Set) :=199  RealFunctionOn(f, S) ∧ S ⊆ ℝ ∧200  (∀ A ∈ S, ContinuousWithinDomainAt(f, S, A))201202predicate UniformContinuousOnDomain (f S : Set) :=203  RealFunctionOn(f, S) ∧ S ⊆ ℝ ∧204  (∀ E ∈ ℝ, 0 < E →205    ∃ D ∈ ℝ, 0 < D ∧206      ∀ X ∈ ℝ, (X ∈ S →207        ∀ Y ∈ ℝ, (Y ∈ S → (X ∈ openBall(Y, D) →208          f(X) ∈ openBall(f(Y), E)))))209210theorem RealFunctionOn.of_function_between (f D S : Set)211  requires function : f : D → ℝ212  requires domainReal : D ⊆ ℝ213  requires subset : S ⊆ D214  shows RealFunctionOn(f, S)215proof216  witness D217  refine ⟨domainReal, subset, function⟩218219theorem RealFunctionOn.apply_real (f S : Set, X : Real)220  requires function : RealFunctionOn(f, S)221  requires member : X ∈ S222  shows Real(f(X))223proof224  rcases function with ⟨D, domainReal, subset, graphFunction⟩225  have memberD := subset with X, member226  exact FunctionBetween.apply_closed with graphFunction, memberD227228theorem ContinuousOn.domain (f S : Set)229  requires continuous : ContinuousOn(f, S)230  shows ContinuousOnDomain(f, S)231proof232  rcases continuous with ⟨function, subset, atPoints⟩233  have realFunction : RealFunctionOn(f, S)234    exact RealFunctionOn.of_function_between at f, ℝ, S with235      function, Subset.reflexive at ℝ, subset236  unfold ContinuousOnDomain237  refine ⟨realFunction, subset, _⟩238  intros A member239  obtain ⟨functionAt, subsetAt, control⟩ := atPoints with A, member240  have typedA : Real(A)241    have realA := subset with A, member242    unfold Real243    exact realA244  unfold ContinuousWithinDomainAt245  refine ⟨realFunction, subset, member, control⟩246247theorem UniformContinuousOn.domain (f S : Set)248  requires uniform : UniformContinuousOn(f, S)249  shows UniformContinuousOnDomain(f, S)250proof251  rcases uniform with ⟨function, subset, control⟩252  have realFunction : RealFunctionOn(f, S)253    exact RealFunctionOn.of_function_between at f, ℝ, S with254      function, Subset.reflexive at ℝ, subset255  unfold UniformContinuousOnDomain256  refine ⟨realFunction, subset, control⟩257258-- A graph with domain S is admitted directly; no extension to all259-- of ℝ is needed, even when S is a closed interval.260theorem constantFunction.continuous_on_domain (S : Set) (L : Real)261  requires subset : S ⊆ ℝ262  shows ContinuousOnDomain(constantFunction(S, ℝ, L), S)263proof264  have realL : L ∈ ℝ by simp [Real]265  have function := constantFunction.function at S, ℝ, L with realL266  have realFunction := RealFunctionOn.of_function_between at267    constantFunction(S, ℝ, L), S, S with268      function, subset, Subset.reflexive at S269  unfold ContinuousOnDomain270  refine ⟨realFunction, subset, _⟩271  intros A memberA272  have realA : Real(A)273    have inReals := subset with A, memberA274    unfold Real275    exact inReals276  unfold ContinuousWithinDomainAt277  refine ⟨realFunction, subset, memberA, _⟩278  intros E realE positive279  witness E280  refine ⟨realE, positive, _⟩281  intros X realX memberX near282  have valueX := constantFunction.apply with memberX, realL283  have valueA := constantFunction.apply with memberA, realL284  rw [valueX, valueA]285  exact openBall.center with positive286287-- DomainSequentialContinuity288theorem ContinuousWithinDomainAt.converges_in (f u S D : Set) (L : Real)289  requires continuous : ContinuousWithinDomainAt(f, S, L)290  requires function : f : D → ℝ291  requires subset : S ⊆ D292  requires converges : ConvergesTo(u, L)293  requires terms : TermsIn(u, S)294  shows ConvergesTo(compose(f, u, ℕ, D, ℝ), f(L))295proof296  rcases continuous with ⟨domainFunction, subsetReal, memberL, control⟩297  have sequence := ConvergesTo.sequence with converges298  unfold RealSequence at sequence299  have values : ∀ j ∈ ℕ, u(j) ∈ D300    intros j naturalJ301    have termS := terms with j, naturalJ302    exact subset with u(j), termS303  have sequenceD := FunctionBetween.codomain_of_values with sequence, values304  have limitD : L ∈ D by exact subset with L, memberL305  have imageReal := FunctionBetween.apply_closed with function, limitD306  constructor307  . unfold RealSequence308    exact compose.function with sequenceD, function309  . intros E realE positive310    obtain ⟨R, realR, positiveR, maps⟩ :=311      control with E, realE, positive312    obtain ⟨N, naturalN, close⟩ := ConvergesTo.eventually with converges, positiveR313    witness N314    constructor315    . exact naturalN316    . intros n indexNatural afterN317      have termReal := FunctionBetween.apply_closed with sequence, indexNatural318      have member := terms with n, indexNatural319      have near := close with n, indexNatural, afterN320      have mapped := maps with u(n), termReal, member, near321      have value : compose(f, u, ℕ, D, ℝ)(n) =322          f(u(n))323        exact compose.apply with sequenceD, function, indexNatural324      rwa value325326theorem ContinuousOnDomain.converges_in (f u S D : Set) (L : Real)327  requires continuous : ContinuousOnDomain(f, S)328  requires function : f : D → ℝ329  requires subset : S ⊆ D330  requires limitMember : L ∈ S331  requires converges : ConvergesTo(u, L)332  requires terms : TermsIn(u, S)333  shows ConvergesTo(compose(f, u, ℕ, D, ℝ), f(L))334proof335  rcases continuous with ⟨domainFunction, subsetReal, atPoints⟩336  have atLimit := atPoints with L, limitMember337  exact ContinuousWithinDomainAt.converges_in with atLimit, function, subset, converges, terms338339theorem ContinuousOnDomain.nearby_compact_images (f S D u v : Set)340  requires continuous : ContinuousOnDomain(f, S)341  requires function : f : D → ℝ342  requires subset : S ⊆ D343  requires compact : SequentiallyCompact(S)344  requires sequence : RealSequence(u)345  requires termsU : TermsIn(u, S)346  requires termsV : TermsIn(v, S)347  requires close : AsymptoticallyClose(u, v)348  shows ∃ k, StrictlyIncreasingNat(k) ∧349    ∃ L ∈ ℝ, L ∈ S ∧350      ConvergesTo(compose(f, subsequence(u, k), ℕ, D, ℝ), f(L)) ∧351      ConvergesTo(compose(f, subsequence(v, k), ℕ, D, ℝ), f(L))352proof353  obtain ⟨k, increasing, L, realL, member, convergesU, convergesV⟩ := SequentiallyCompact.nearby_subsequences with354    compact, sequence, termsU, close355  have selectedU := TermsIn.subsequence with sequence, termsU, increasing356  rcases close with ⟨sequenceAgain, sequenceV, eventually⟩357  have selectedV := TermsIn.subsequence with sequenceV, termsV, increasing358  have mappedU := ContinuousOnDomain.converges_in with359    continuous, function, subset, member, convergesU, selectedU360  have mappedV := ContinuousOnDomain.converges_in with361    continuous, function, subset, member, convergesV, selectedV362  witness k363  constructor364  . exact increasing365  . witness L366    refine ⟨realL, member, mappedU, mappedV⟩367368-- Section: DomainHeineCantor369theorem ContinuousOnDomain.nonuniform_tolerance (f S : Set)370  requires continuous : ContinuousOnDomain(f, S)371  requires notUniform : ¬UniformContinuousOnDomain(f, S)372  shows ∃ E ∈ ℝ, (0 < E ∧373    ∀ D ∈ ℝ, (0 < D →374      ¬(∀ X ∈ ℝ, (X ∈ S →375        ∀ Y ∈ ℝ, (Y ∈ S →376          (X ∈ openBall(Y, D) →377            f(X) ∈ openBall(f(Y), E)))))))378proof379  rcases continuous with ⟨function, subset, atPoints⟩380  by_contra noTolerance381  apply notUniform382  constructor383  . exact function384  . constructor385    . exact subset386    . intros E realE positive387      have radiusExists : ∃ D ∈ ℝ, (0 < D ∧388          ∀ X ∈ ℝ, (X ∈ S →389            ∀ Y ∈ ℝ, (Y ∈ S →390              (X ∈ openBall(Y, D) →391                f(X) ∈ openBall(f(Y), E)))))392        by_contra noRadius393        apply noTolerance394        witness E395        constructor396        . exact realE397        . constructor398          . exact positive399          . intros D realD positiveD maps400            apply noRadius401            witness D402            refine ⟨realD, positiveD, maps⟩403      exact radiusExists404405-- This is the textbook epsilon that defeats every delta, with the real406-- witnesses and interval membership written out.407theorem ContinuousOnDomain.nonuniform_pairs (f S : Set)408  requires continuous : ContinuousOnDomain(f, S)409  requires notUniform : ¬UniformContinuousOnDomain(f, S)410  shows ∃ E ∈ ℝ, (0 < E ∧411    ∀ D ∈ ℝ, (0 < D →412      ∃ X ∈ ℝ, ∃ Y ∈ ℝ, UniformFailurePair(f, S, E, D, X, Y)))413proof414  obtain ⟨E, realE, positiveE, noRadius⟩ := ContinuousOnDomain.nonuniform_tolerance with415    continuous, notUniform416  witness E417  constructor418  . exact realE419  . constructor420    . exact positiveE421    . intros D realD positiveD422      have noMaps := noRadius with D, realD, positiveD423      have bad : ∃ X ∈ ℝ, ∃ Y ∈ ℝ, (424          X ∈ S ∧ Y ∈ S ∧ X ∈ openBall(Y, D) ∧425            ¬(f(X) ∈ openBall(f(Y), E)))426        by_contra noBad427        apply noMaps428        intros P realP memberP Q realQ memberQ near429        by_contra notNear430        apply noBad431        witness P432        constructor433        . exact realP434        . witness Q435          refine ⟨realQ, memberP, memberQ, near, notNear⟩436      obtain ⟨X, realX, Y, realY, memberX, memberY, near, far⟩ := bad437      witness X438      constructor439      . exact realX440      . witness Y441        constructor442        . exact realY443        . unfold UniformFailurePair444          refine ⟨memberX, memberY, near, far⟩445446-- DomainHeineCantor447theorem ContinuousOnDomain.uniform_of_sequentially_compact (f S : Set)448  requires continuous : ContinuousOnDomain(f, S)449  requires compact : SequentiallyCompact(S)450  shows UniformContinuousOnDomain(f, S)451proof452  by_contra notUniform453  obtain ⟨E, realE, positiveE, witnesses⟩ := ContinuousOnDomain.nonuniform_pairs with continuous, notUniform454  have continuousAgain := continuous455  rcases continuous with ⟨domainFunction, subsetReal, atPoints⟩456  rcases domainFunction with ⟨D, domainReal, subset, graphFunction⟩457  obtain ⟨termsFirst, termsSecond, close, far⟩ := failureWitnesses.properties with witnesses458  have sequenceSecond := failureSecondSequence.sequence with witnesses459  obtain ⟨k, increasing, L, realL, memberL, mapsSecond, mapsFirst⟩ := ContinuousOnDomain.nearby_compact_images with460    continuousAgain, graphFunction, subset, compact, sequenceSecond, termsSecond, termsFirst, close461  have function : f : D → ℝ by exact graphFunction462  have memberD : L ∈ D by exact subset with L, memberL463  have mappedReal : Real(f(L))464    have realImage := FunctionBetween.apply_closed with function, memberD465    unfold Real466    exact realImage467  obtain ⟨N, naturalN, near⟩ := ConvergesTo.eventually_near_each_other with mapsSecond, mapsFirst, positiveE468  have typedN : Nat(N) by exact nat.omega.backward at N with naturalN469  have afterN := LessEqual.reflexive with typedN470  have selectedNear := near with N, naturalN, afterN471  have selectedSecondSequence := subsequence.sequence with sequenceSecond, increasing472  have termsSelectedSecond := TermsIn.subsequence with sequenceSecond, termsSecond, increasing473  have secondValues : ∀ j ∈ ℕ,474      subsequence(failureSecondSequence(f, S, E), k)(j) ∈ D475    intros j naturalJ476    have memberS := termsSelectedSecond with j, naturalJ477    exact subset with subsequence(failureSecondSequence(f, S, E), k)(j), memberS478  unfold RealSequence at selectedSecondSequence479  have selectedSecondDomain := FunctionBetween.codomain_of_values with selectedSecondSequence, secondValues480  have sequenceFirst := failureFirstSequence.sequence with witnesses481  have selectedFirstSequence := subsequence.sequence with sequenceFirst, increasing482  have termsSelectedFirst := TermsIn.subsequence with sequenceFirst, termsFirst, increasing483  have firstValues : ∀ j ∈ ℕ,484      subsequence(failureFirstSequence(f, S, E), k)(j) ∈ D485    intros j naturalJ486    have memberS := termsSelectedFirst with j, naturalJ487    exact subset with subsequence(failureFirstSequence(f, S, E), k)(j), memberS488  unfold RealSequence at selectedFirstSequence489  have selectedFirstDomain := FunctionBetween.codomain_of_values with selectedFirstSequence, firstValues490  have mappedSecond := compose.apply with selectedSecondDomain, function, naturalN491  have mappedFirst := compose.apply with selectedFirstDomain, function, naturalN492  rw [mappedFirst, mappedSecond] at selectedNear493  have chosenSecond := subsequence.value with sequenceSecond, increasing494  have chosenFirst := subsequence.value with sequenceFirst, increasing495  rw [chosenFirst, chosenSecond] at selectedNear496  have selectorFunction := StrictlyIncreasingNat.function with increasing497  have selectedNatural := FunctionBetween.apply_closed with selectorFunction, naturalN498  have contradiction := far with k[N], selectedNatural499  exact contradiction with selectedNear500501theorem closedInterval.heine_cantor_on_domain (f : Set, A B : Real)502  requires continuous : ContinuousOnDomain(f, closedInterval(A, B))503  shows UniformContinuousOnDomain(f, closedInterval(A, B))504proof505  have compact := closedInterval.sequentially_compact at A, B with506    *{2}507  exact ContinuousOnDomain.uniform_of_sequentially_compact with continuous, compact508