Analysis I, Section 9.9: Uniform continuity

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

open Chapter6 Filternamespace Chapter9declaration uses 'sorry'example : ContinuousOn (fun x:ℝ ↦ 1/x) (.Icc 0 2) := ⊢ ContinuousOn (fun x => 1 / x) (Set.Icc 0 2) All goals completed! 🐙declaration uses 'sorry'example : ¬ BddOn (fun x:ℝ ↦ 1/x) (.Icc 0 2) := ⊢ ¬BddOn (fun x => 1 / x) (Set.Icc 0 2) All goals completed! 🐙

Example 9.9.1

declaration uses 'sorry'example (x : ℝ) : let f : ℝ → ℝ := fun x ↦ 1/x let ε : ℝ := 0.1 let x₀ : ℝ := 1 let δ : ℝ := 1/11 |x-x₀| ≤ δ → |f x - f x₀| ≤ ε := x:ℝ⊢ let f := fun x => 1 / x; let ε := 0.1; let x₀ := 1; let δ := 1 / 11; |x - x₀| ≤ δ → |f x - f x₀| ≤ ε x:ℝf:ℝ → ℝ := fun x => 1 / xε:ℝ := 0.1x₀:ℝ := 1δ:ℝ := 1 / 11⊢ |x - x₀| ≤ δ → |f x - f x₀| ≤ ε All goals completed! 🐙
declaration uses 'sorry'example (x:ℝ) : let f : ℝ → ℝ := fun x ↦ 1/x let ε : ℝ := 0.1 let x₀ : ℝ := 0.1 let δ : ℝ := 1/1010 |x-x₀| ≤ δ → |f x - f x₀| ≤ ε := x:ℝ⊢ let f := fun x => 1 / x; let ε := 0.1; let x₀ := 0.1; let δ := 1 / 1010; |x - x₀| ≤ δ → |f x - f x₀| ≤ ε x:ℝf:ℝ → ℝ := fun x => 1 / xε:ℝ := 0.1x₀:ℝ := 0.1δ:ℝ := 1 / 1010⊢ |x - x₀| ≤ δ → |f x - f x₀| ≤ ε -- need the `-merge` flag due to the collision of `ε` and `x₀` All goals completed! 🐙declaration uses 'sorry'example (x:ℝ) : let g : ℝ → ℝ := fun x ↦ 2*x let ε : ℝ := 0.1 let x₀ : ℝ := 1 let δ : ℝ := 0.05 |x-x₀| ≤ δ → |g x - g x₀| ≤ ε := x:ℝ⊢ let g := fun x => 2 * x; let ε := 0.1; let x₀ := 1; let δ := 5e-2; |x - x₀| ≤ δ → |g x - g x₀| ≤ ε x:ℝg:ℝ → ℝ := fun x => 2 * xε:ℝ := 0.1x₀:ℝ := 1δ:ℝ := 5e-2⊢ |x - x₀| ≤ δ → |g x - g x₀| ≤ ε All goals completed! 🐙declaration uses 'sorry'example (x₀ x : ℝ) : let g : ℝ → ℝ := fun x ↦ 2*x let ε : ℝ := 0.1 let δ : ℝ := 0.05 |x-x₀| ≤ δ → |g x - g x₀| ≤ ε := x₀:ℝx:ℝ⊢ let g := fun x => 2 * x; let ε := 0.1; let δ := 5e-2; |x - x₀| ≤ δ → |g x - g x₀| ≤ ε x₀:ℝx:ℝg:ℝ → ℝ := fun x => 2 * xε:ℝ := 0.1δ:ℝ := 5e-2⊢ |x - x₀| ≤ δ → |g x - g x₀| ≤ ε All goals completed! 🐙

Definition 9.9.2. Here we use the Mathlib term UniformContinuousOn.{ua, ub} {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] (f : α → β) (s : Set α) : PropUniformContinuousOn

theorem UniformContinuousOn.iff (f: ℝ → ℝ) (X:Set ℝ) : UniformContinuousOn f X ↔ ∀ ε > (0:ℝ), ∃ δ > (0:ℝ), ∀ x₀ ∈ X, ∀ x ∈ X, δ.Close x x₀ → ε.Close (f x) (f x₀) := f:ℝ → ℝX:Set ℝ⊢ UniformContinuousOn f X ↔ ∀ ε > 0, ∃ δ > 0, ∀ x₀ ∈ X, ∀ x ∈ X, δ.Close x x₀ → ε.Close (f x) (f x₀) f:ℝ → ℝX:Set ℝ⊢ (∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, ∀ y ∈ X, dist x y ≤ δ → dist (f x) (f y) ≤ ε) ↔ ∀ ε > 0, ∃ δ > 0, ∀ x₀ ∈ X, ∀ x ∈ X, dist x x₀ ≤ δ → dist (f x) (f x₀) ≤ ε All goals completed! 🐙
theorem declaration uses 'sorry'ContinuousOn.ofUniformContinuousOn {X:Set ℝ} (f: ℝ → ℝ) (hf: UniformContinuousOn f X) : ContinuousOn f X := X:Set ℝf:ℝ → ℝhf:UniformContinuousOn f X⊢ ContinuousOn f X All goals completed! 🐙declaration uses 'sorry'example : ¬ UniformContinuousOn (fun x:ℝ ↦ 1/x) (Set.Icc 0 2) := ⊢ ¬UniformContinuousOn (fun x => 1 / x) (Set.Icc 0 2) All goals completed! 🐙end Chapter9

Definition 9.9.5. This is similar but not identical to Unknown constant `Real.close_seq`Real.close_seq from Section 6.1.

abbrev Real.CloseSeqs (ε:ℝ) (a b: Chapter6.Sequence) : Prop := (a.m = b.m) ∧ ∀ n ≥ a.m, ε.Close (a n) (b n)
abbrev Real.EventuallyCloseSeqs (ε:ℝ) (a b: Chapter6.Sequence) : Prop := ∃ N ≥ a.m, ε.CloseSeqs (a.from N) (b.from N)abbrev Chapter6.Sequence.equiv (a b: Sequence) : Prop := ∀ ε > (0:ℝ), ε.EventuallyCloseSeqs a b

Remark 9.9.6

theorem declaration uses 'sorry'Chapter6.Sequence.equiv_iff_rat (a b: Sequence) : a.equiv b ↔ ∀ ε > (0:ℚ), (ε:ℝ).EventuallyCloseSeqs a b := a:Sequenceb:Sequence⊢ a.equiv b ↔ ∀ ε > 0, (↑ε).EventuallyCloseSeqs a b All goals completed! 🐙

Lemma 9.9.7 / Exercise 9.9.1

theorem declaration uses 'sorry'Chapter6.Sequence.equiv_iff (a b: Sequence) : a.equiv b ↔ atTop.Tendsto (fun n ↦ a n - b n) (nhds 0) := a:Sequenceb:Sequence⊢ a.equiv b ↔ Tendsto (fun n => a.seq n - b.seq n) atTop (nhds 0) All goals completed! 🐙
namespace Chapter9

Proposition 9.9.8 / Exercise 9.9.2

theorem declaration uses 'sorry'UniformContinuousOn.iff_preserves_equiv {X:Set ℝ} (f: ℝ → ℝ) : UniformContinuousOn f X ↔ ∀ x y: ℕ → ℝ, (∀ n, x n ∈ X) → (∀ n, y n ∈ X) → (x:Sequence).equiv (y:Sequence) → (f ∘ x:Sequence).equiv (f ∘ y:Sequence) := X:Set ℝf:ℝ → ℝ⊢ UniformContinuousOn f X ↔ ∀ (x y : ℕ → ℝ), (∀ (n : ℕ), x n ∈ X) → (∀ (n : ℕ), y n ∈ X) → (↑x).equiv ↑y → (↑(f ∘ x)).equiv ↑(f ∘ y) All goals completed! 🐙

Remark 9.9.9

theorem declaration uses 'sorry'Chapter6.Sequence.equiv_const (x₀: ℝ) (x:ℕ → ℝ) : atTop.Tendsto x (nhds x₀) ↔ (x:Sequence).equiv (fun n:ℕ ↦ x₀:Sequence) := x₀:ℝx:ℕ → ℝ⊢ Tendsto x atTop (nhds x₀) ↔ (↑x).equiv ↑fun n => x₀ All goals completed! 🐙

Example 9.9.10

noncomputable abbrev f_9_9_10 : ℝ → ℝ := fun x ↦ 1/x
declaration uses 'sorry'example : (fun n:ℕ ↦ 1/(n+1:ℝ):Sequence).equiv (fun n:ℕ ↦ 1/(2*(n+1):ℝ):Sequence) := ⊢ (↑fun n => 1 / (↑n + 1)).equiv ↑fun n => 1 / (2 * (↑n + 1)) All goals completed! 🐙declaration uses 'sorry'example (n:ℕ) : 1/(n+1:ℝ) ∈ Set.Ioo 0 2 := n:ℕ⊢ 1 / (↑n + 1) ∈ Set.Ioo 0 2 All goals completed! 🐙declaration uses 'sorry'example (n:ℕ) : 1/(2*(n+1):ℝ) ∈ Set.Ioo 0 2 := n:ℕ⊢ 1 / (2 * (↑n + 1)) ∈ Set.Ioo 0 2 All goals completed! 🐙declaration uses 'sorry'example : ¬ (fun n:ℕ ↦ f_9_9_10 (1/(n+1:ℝ)):Sequence).equiv (fun n:ℕ ↦ f_9_9_10 (1/(2*(n+1):ℝ)):Sequence) := ⊢ ¬(↑fun n => f_9_9_10 (1 / (↑n + 1))).equiv ↑fun n => f_9_9_10 (1 / (2 * (↑n + 1))) All goals completed! 🐙declaration uses 'sorry'example : ¬ UniformContinuousOn f_9_9_10 (.Ioo 0 2) := ⊢ ¬UniformContinuousOn f_9_9_10 (Set.Ioo 0 2) All goals completed! 🐙

Example 9.9.11

abbrev f_9_9_11 : ℝ → ℝ := fun x ↦ x^2
declaration uses 'sorry'example : ((fun n:ℕ ↦ (n+1:ℝ)):Sequence).equiv ((fun n:ℕ ↦ (n+1)+1/(n+1:ℝ)):Sequence) := ⊢ (↑fun n => ↑n + 1).equiv ↑fun n => ↑n + 1 + 1 / (↑n + 1) All goals completed! 🐙declaration uses 'sorry'example : ¬ ((fun n:ℕ ↦ f_9_9_11 (n+1:ℝ)):Sequence).equiv ((fun n:ℕ ↦ f_9_9_11 ((n+1)+1/(n+1:ℝ))):Sequence) := ⊢ ¬(↑fun n => f_9_9_11 (↑n + 1)).equiv ↑fun n => f_9_9_11 (↑n + 1 + 1 / (↑n + 1)) All goals completed! 🐙declaration uses 'sorry'example : ¬ UniformContinuousOn f_9_9_11 .univ := ⊢ ¬UniformContinuousOn f_9_9_11 Set.univ All goals completed! 🐙

Proposition 9.9.12 / Exercise 9.9.3

theorem declaration uses 'sorry'UniformContinuousOn.ofCauchy {X:Set ℝ} (f: ℝ → ℝ) (hf: UniformContinuousOn f X) {x: ℕ → ℝ} (hx: (x:Sequence).IsCauchy) (hmem : ∀ n, x n ∈ X) : (f ∘ x:Sequence).IsCauchy := X:Set ℝf:ℝ → ℝhf:UniformContinuousOn f Xx:ℕ → ℝhx:(↑x).IsCauchyhmem:∀ (n : ℕ), x n ∈ X⊢ (↑(f ∘ x)).IsCauchy All goals completed! 🐙

Example 9.9.13

declaration uses 'sorry'example : ((fun n:ℕ ↦ 1/(n+1:ℝ)):Sequence).IsCauchy := ⊢ (↑fun n => 1 / (↑n + 1)).IsCauchy All goals completed! 🐙
declaration uses 'sorry'example (n:ℕ) : 1/(n+1:ℝ) ∈ Set.Ioo 0 2 := n:ℕ⊢ 1 / (↑n + 1) ∈ Set.Ioo 0 2 All goals completed! 🐙declaration uses 'sorry'example : ¬ ((fun n:ℕ ↦ f_9_9_10 (1/(n+1:ℝ))):Sequence).IsCauchy := ⊢ ¬(↑fun n => f_9_9_10 (1 / (↑n + 1))).IsCauchy All goals completed! 🐙declaration uses 'sorry'example : ¬ UniformContinuousOn f_9_9_10 (Set.Ioo 0 2) := ⊢ ¬UniformContinuousOn f_9_9_10 (Set.Ioo 0 2) All goals completed! 🐙

Corollary 9.9.14 / Exercise 9.9.4

theorem declaration uses 'sorry'UniformContinuousOn.limit_at_adherent {X:Set ℝ} (f: ℝ → ℝ) (hf: UniformContinuousOn f X) {x₀:ℝ} (hx₀: AdherentPt x₀ X) : ∃ L:ℝ, (nhdsWithin x₀ X).Tendsto f (nhds L) := X:Set ℝf:ℝ → ℝhf:UniformContinuousOn f Xx₀:ℝhx₀:AdherentPt x₀ X⊢ ∃ L, Tendsto f (nhdsWithin x₀ X) (nhds L) All goals completed! 🐙

Proposition 9.9.15 / Exercise 9.9.5

theorem declaration uses 'sorry'UniformContinuousOn.of_bounded {E X:Set ℝ} {f: ℝ → ℝ} (hf: UniformContinuousOn f X) (hEX: E ⊆ X) (hE: Bornology.IsBounded E) : Bornology.IsBounded (f '' E) := E:Set ℝX:Set ℝf:ℝ → ℝhf:UniformContinuousOn f XhEX:E ⊆ XhE:Bornology.IsBounded E⊢ Bornology.IsBounded (f '' E) All goals completed! 🐙

Theorem 9.9.16

theorem declaration uses 'sorry'UniformContinuousOn.of_continuousOn {a b:ℝ} {f:ℝ → ℝ} (hcont: ContinuousOn f (.Icc a b)) : UniformContinuousOn f (.Icc a b) := a:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)⊢ UniformContinuousOn f (Set.Icc a b) -- This proof is written to follow the structure of the original text. a:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)h:¬UniformContinuousOn f (Set.Icc a b)⊢ False; a:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)h:¬∀ (x y : ℕ → ℝ), (∀ (n : ℕ), x n ∈ Set.Icc a b) → (∀ (n : ℕ), y n ∈ Set.Icc a b) → (↑x).equiv ↑y → (↑(f ∘ x)).equiv ↑(f ∘ y)⊢ False a:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)h:∃ x, (∀ (n : ℕ), x n ∈ Set.Icc a b) ∧ ∃ x_1, (∀ (n : ℕ), x_1 n ∈ Set.Icc a b) ∧ (↑x).equiv ↑x_1 ∧ ∃ x_2, 0 < x_2 ∧ ∀ (x_3 : ℤ), 0 ≤ x_3 → ∃ x_4, 0 ≤ x_4 ∧ x_3 ≤ x_4 ∧ x_2 < dist (if 0 ≤ x_4 ∧ x_3 ≤ x_4 then if 0 ≤ x_4 then f (x x_4.toNat) else 0 else 0) (if 0 ≤ x_4 ∧ x_3 ≤ x_4 then if 0 ≤ x_4 then f (x_1 x_4.toNat) else 0 else 0)⊢ False a:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a by:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:(↑x).equiv ↑yε:ℝhε:0 < εh:∀ (x_1 : ℤ), 0 ≤ x_1 → ∃ x_2, 0 ≤ x_2 ∧ x_1 ≤ x_2 ∧ ε < dist (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (x x_2.toNat) else 0 else 0) (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (y x_2.toNat) else 0 else 0)⊢ False a:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a by:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:(↑x).equiv ↑yε:ℝhε:0 < εh:∀ (x_1 : ℤ), 0 ≤ x_1 → ∃ x_2, 0 ≤ x_2 ∧ x_1 ≤ x_2 ∧ ε < dist (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (x x_2.toNat) else 0 else 0) (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (y x_2.toNat) else 0 else 0)E:Set ℕ := {n | ¬Real.Close _fvar.201571 (@_fvar.19113 (@_fvar.201524 n)) (@_fvar.19113 (@_fvar.201542 n))}⊢ False have hE : Infinite E := a:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)⊢ UniformContinuousOn f (Set.Icc a b) a:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a by:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:(↑x).equiv ↑yε:ℝhε:0 < εh:∀ (x_1 : ℤ), 0 ≤ x_1 → ∃ x_2, 0 ≤ x_2 ∧ x_1 ≤ x_2 ∧ ε < dist (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (x x_2.toNat) else 0 else 0) (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (y x_2.toNat) else 0 else 0)E:Set ℕ := {n | ¬Real.Close _fvar.201571 (@_fvar.19113 (@_fvar.201524 n)) (@_fvar.19113 (@_fvar.201542 n))}⊢ ¬Finite ↑E a:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a by:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:(↑x).equiv ↑yε:ℝhε:0 < εh:∀ (x_1 : ℤ), 0 ≤ x_1 → ∃ x_2, 0 ≤ x_2 ∧ x_1 ≤ x_2 ∧ ε < dist (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (x x_2.toNat) else 0 else 0) (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (y x_2.toNat) else 0 else 0)E:Set ℕ := {n | ¬Real.Close _fvar.201571 (@_fvar.19113 (@_fvar.201524 n)) (@_fvar.19113 (@_fvar.201542 n))}this:Finite ↑E⊢ False replace : ε.EventuallyCloseSeqs (fun n ↦ f (x n):Sequence) (fun n ↦ f (y n):Sequence) := a:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)⊢ UniformContinuousOn f (Set.Icc a b) All goals completed! 🐙 All goals completed! 🐙 a:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a by:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:(↑x).equiv ↑yε:ℝhε:0 < εh:∀ (x_1 : ℤ), 0 ≤ x_1 → ∃ x_2, 0 ≤ x_2 ∧ x_1 ≤ x_2 ∧ ε < dist (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (x x_2.toNat) else 0 else 0) (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (y x_2.toNat) else 0 else 0)E:Set ℕ := {n | ¬Real.Close _fvar.201571 (@_fvar.19113 (@_fvar.201524 n)) (@_fvar.19113 (@_fvar.201542 n))}hE:Infinite ↑_fvar.201604 := ?_mvar.201976this:Countable ↑E⊢ False a:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a by:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:(↑x).equiv ↑yε:ℝhε:0 < εh:∀ (x_1 : ℤ), 0 ≤ x_1 → ∃ x_2, 0 ≤ x_2 ∧ x_1 ≤ x_2 ∧ ε < dist (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (x x_2.toNat) else 0 else 0) (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (y x_2.toNat) else 0 else 0)E:Set ℕ := {n | ¬Real.Close _fvar.201571 (@_fvar.19113 (@_fvar.201524 n)) (@_fvar.19113 (@_fvar.201542 n))}hE:Infinite ↑_fvar.201604 := ?_mvar.201976this:Countable ↑En:ℕ → ℕ := Nat.nth _fvar.201604⊢ False a:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a by:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:(↑x).equiv ↑yε:ℝhε:0 < εh:∀ (x_1 : ℤ), 0 ≤ x_1 → ∃ x_2, 0 ≤ x_2 ∧ x_1 ≤ x_2 ∧ ε < dist (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (x x_2.toNat) else 0 else 0) (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (y x_2.toNat) else 0 else 0)E:Set ℕ := {n | ¬Real.Close _fvar.201571 (@_fvar.19113 (@_fvar.201524 n)) (@_fvar.19113 (@_fvar.201542 n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth _fvar.201604⊢ False have hmono : StrictMono n := a:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)⊢ UniformContinuousOn f (Set.Icc a b) All goals completed! 🐙 a:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a by:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:(↑x).equiv ↑yε:ℝhε:0 < εh:∀ (x_1 : ℤ), 0 ≤ x_1 → ∃ x_2, 0 ≤ x_2 ∧ x_1 ≤ x_2 ∧ ε < dist (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (x x_2.toNat) else 0 else 0) (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (y x_2.toNat) else 0 else 0)E:Set ℕ := {n | ¬Real.Close _fvar.201571 (@_fvar.19113 (@_fvar.201524 n)) (@_fvar.19113 (@_fvar.201542 n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth _fvar.201604hmono:StrictMono _fvar.252778 := ?_mvar.252900hmem:∀ (j : ℕ), @_fvar.252778 j ∈ _fvar.201604 := fun j => Nat.nth_mem_of_infinite _fvar.252774 j⊢ False have hsep (j:ℕ) : |f (x (n j)) - f (y (n j))| > ε := a:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)⊢ UniformContinuousOn f (Set.Icc a b) a:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a by:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:(↑x).equiv ↑yε:ℝhε:0 < εh:∀ (x_1 : ℤ), 0 ≤ x_1 → ∃ x_2, 0 ≤ x_2 ∧ x_1 ≤ x_2 ∧ ε < dist (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (x x_2.toNat) else 0 else 0) (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (y x_2.toNat) else 0 else 0)E:Set ℕ := {n | ¬Real.Close _fvar.201571 (@_fvar.19113 (@_fvar.201524 n)) (@_fvar.19113 (@_fvar.201542 n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth _fvar.201604hmono:StrictMono _fvar.252778 := ?_mvar.252900j:ℕhmem:n j ∈ E⊢ |f (x (n j)) - f (y (n j))| > ε All goals completed! 🐙 a:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a by:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:(↑x).equiv ↑yε:ℝhε:0 < εh:∀ (x_1 : ℤ), 0 ≤ x_1 → ∃ x_2, 0 ≤ x_2 ∧ x_1 ≤ x_2 ∧ ε < dist (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (x x_2.toNat) else 0 else 0) (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (y x_2.toNat) else 0 else 0)E:Set ℕ := {n | ¬Real.Close _fvar.201571 (@_fvar.19113 (@_fvar.201524 n)) (@_fvar.19113 (@_fvar.201542 n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth _fvar.201604hmono:StrictMono _fvar.252778 := ?_mvar.252900hmem:∀ (j : ℕ), @_fvar.252778 j ∈ _fvar.201604 := fun j => Nat.nth_mem_of_infinite _fvar.252774 jhsep:∀ (j : ℕ), |@_fvar.19113 (@_fvar.201524 (@_fvar.252778 j)) - @_fvar.19113 (@_fvar.201542 (@_fvar.252778 j))| > _fvar.201571 := fun j => @?_mvar.253348 jhxmem:∀ (j : ℕ), x (n j) ∈ Set.Icc a b⊢ False a:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a by:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:(↑x).equiv ↑yε:ℝhε:0 < εh:∀ (x_1 : ℤ), 0 ≤ x_1 → ∃ x_2, 0 ≤ x_2 ∧ x_1 ≤ x_2 ∧ ε < dist (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (x x_2.toNat) else 0 else 0) (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (y x_2.toNat) else 0 else 0)E:Set ℕ := {n | ¬Real.Close _fvar.201571 (@_fvar.19113 (@_fvar.201524 n)) (@_fvar.19113 (@_fvar.201542 n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth _fvar.201604hmono:StrictMono _fvar.252778 := ?_mvar.252900hmem:∀ (j : ℕ), @_fvar.252778 j ∈ _fvar.201604 := fun j => Nat.nth_mem_of_infinite _fvar.252774 jhsep:∀ (j : ℕ), |@_fvar.19113 (@_fvar.201524 (@_fvar.252778 j)) - @_fvar.19113 (@_fvar.201542 (@_fvar.252778 j))| > _fvar.201571 := fun j => @?_mvar.253348 jhxmem:∀ (j : ℕ), x (n j) ∈ Set.Icc a bhymem:∀ (j : ℕ), y (n j) ∈ Set.Icc a b⊢ False a:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a by:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:(↑x).equiv ↑yε:ℝhε:0 < εh:∀ (x_1 : ℤ), 0 ≤ x_1 → ∃ x_2, 0 ≤ x_2 ∧ x_1 ≤ x_2 ∧ ε < dist (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (x x_2.toNat) else 0 else 0) (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (y x_2.toNat) else 0 else 0)E:Set ℕ := {n | ¬Real.Close _fvar.201571 (@_fvar.19113 (@_fvar.201524 n)) (@_fvar.19113 (@_fvar.201542 n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth _fvar.201604hmono:StrictMono _fvar.252778 := ?_mvar.252900hmem:∀ (j : ℕ), @_fvar.252778 j ∈ _fvar.201604 := fun j => Nat.nth_mem_of_infinite _fvar.252774 jhsep:∀ (j : ℕ), |@_fvar.19113 (@_fvar.201524 (@_fvar.252778 j)) - @_fvar.19113 (@_fvar.201542 (@_fvar.252778 j))| > _fvar.201571 := fun j => @?_mvar.253348 jhxmem:∀ (j : ℕ), x (n j) ∈ Set.Icc a bhymem:∀ (j : ℕ), y (n j) ∈ Set.Icc a bhclosed:IsClosed (Set.Icc a b)⊢ False a:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a by:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:(↑x).equiv ↑yε:ℝhε:0 < εh:∀ (x_1 : ℤ), 0 ≤ x_1 → ∃ x_2, 0 ≤ x_2 ∧ x_1 ≤ x_2 ∧ ε < dist (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (x x_2.toNat) else 0 else 0) (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (y x_2.toNat) else 0 else 0)E:Set ℕ := {n | ¬Real.Close _fvar.201571 (@_fvar.19113 (@_fvar.201524 n)) (@_fvar.19113 (@_fvar.201542 n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth _fvar.201604hmono:StrictMono _fvar.252778 := ?_mvar.252900hmem:∀ (j : ℕ), @_fvar.252778 j ∈ _fvar.201604 := fun j => Nat.nth_mem_of_infinite _fvar.252774 jhsep:∀ (j : ℕ), |@_fvar.19113 (@_fvar.201524 (@_fvar.252778 j)) - @_fvar.19113 (@_fvar.201542 (@_fvar.252778 j))| > _fvar.201571 := fun j => @?_mvar.253348 jhxmem:∀ (j : ℕ), x (n j) ∈ Set.Icc a bhymem:∀ (j : ℕ), y (n j) ∈ Set.Icc a bhclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)⊢ False a:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a by:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:(↑x).equiv ↑yε:ℝhε:0 < εh:∀ (x_1 : ℤ), 0 ≤ x_1 → ∃ x_2, 0 ≤ x_2 ∧ x_1 ≤ x_2 ∧ ε < dist (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (x x_2.toNat) else 0 else 0) (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (y x_2.toNat) else 0 else 0)E:Set ℕ := {n | ¬Real.Close _fvar.201571 (@_fvar.19113 (@_fvar.201524 n)) (@_fvar.19113 (@_fvar.201542 n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth _fvar.201604hmono:StrictMono _fvar.252778 := ?_mvar.252900hmem:∀ (j : ℕ), @_fvar.252778 j ∈ _fvar.201604 := fun j => Nat.nth_mem_of_infinite _fvar.252774 jhsep:∀ (j : ℕ), |@_fvar.19113 (@_fvar.201524 (@_fvar.252778 j)) - @_fvar.19113 (@_fvar.201542 (@_fvar.252778 j))| > _fvar.201571 := fun j => @?_mvar.253348 jhxmem:∀ (j : ℕ), x (n j) ∈ Set.Icc a bhymem:∀ (j : ℕ), y (n j) ∈ Set.Icc a bhclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)j:ℕ → ℕhj:StrictMono jL:ℝhL:L ∈ Set.Icc a bhconv:Tendsto (fun j_1 => x (n (j j_1))) atTop (nhds L)⊢ False a:ℝb:ℝf:ℝ → ℝx:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a by:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:(↑x).equiv ↑yε:ℝhε:0 < εh:∀ (x_1 : ℤ), 0 ≤ x_1 → ∃ x_2, 0 ≤ x_2 ∧ x_1 ≤ x_2 ∧ ε < dist (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (x x_2.toNat) else 0 else 0) (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (y x_2.toNat) else 0 else 0)E:Set ℕ := {n | ¬Real.Close _fvar.201571 (@_fvar.19113 (@_fvar.201524 n)) (@_fvar.19113 (@_fvar.201542 n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth _fvar.201604hmono:StrictMono _fvar.252778 := ?_mvar.252900hmem:∀ (j : ℕ), @_fvar.252778 j ∈ _fvar.201604 := fun j => Nat.nth_mem_of_infinite _fvar.252774 jhsep:∀ (j : ℕ), |@_fvar.19113 (@_fvar.201524 (@_fvar.252778 j)) - @_fvar.19113 (@_fvar.201542 (@_fvar.252778 j))| > _fvar.201571 := fun j => @?_mvar.253348 jhxmem:∀ (j : ℕ), x (n j) ∈ Set.Icc a bhymem:∀ (j : ℕ), y (n j) ∈ Set.Icc a bhclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)j:ℕ → ℕhj:StrictMono jL:ℝhL:L ∈ Set.Icc a bhconv:Tendsto (fun j_1 => x (n (j j_1))) atTop (nhds L)hcont:?_mvar.258074 := ContinuousOn.continuousWithinAt _fvar.19114 _fvar.257880⊢ False a:ℝb:ℝf:ℝ → ℝx:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a by:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:(↑x).equiv ↑yε:ℝhε:0 < εh:∀ (x_1 : ℤ), 0 ≤ x_1 → ∃ x_2, 0 ≤ x_2 ∧ x_1 ≤ x_2 ∧ ε < dist (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (x x_2.toNat) else 0 else 0) (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (y x_2.toNat) else 0 else 0)E:Set ℕ := {n | ¬Real.Close _fvar.201571 (@_fvar.19113 (@_fvar.201524 n)) (@_fvar.19113 (@_fvar.201542 n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth _fvar.201604hmono:StrictMono _fvar.252778 := ?_mvar.252900hmem:∀ (j : ℕ), @_fvar.252778 j ∈ _fvar.201604 := fun j => Nat.nth_mem_of_infinite _fvar.252774 jhsep:∀ (j : ℕ), |@_fvar.19113 (@_fvar.201524 (@_fvar.252778 j)) - @_fvar.19113 (@_fvar.201542 (@_fvar.252778 j))| > _fvar.201571 := fun j => @?_mvar.253348 jhxmem:∀ (j : ℕ), x (n j) ∈ Set.Icc a bhymem:∀ (j : ℕ), y (n j) ∈ Set.Icc a bhclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)j:ℕ → ℕhj:StrictMono jL:ℝhL:L ∈ Set.Icc a bhconv:Tendsto (fun j_1 => x (n (j j_1))) atTop (nhds L)hcont:?_mvar.258074 := ContinuousOn.continuousWithinAt _fvar.19114 _fvar.257880hconv':?_mvar.258294 := Tendsto.comp_of_continuous _fvar.257880 _fvar.258288 (fun k => @_fvar.255802 (@_fvar.257877 k)) _fvar.257881⊢ False a:ℝb:ℝf:ℝ → ℝx:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a by:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:Tendsto (fun n => (↑x).seq n - (↑y).seq n) atTop (nhds 0)ε:ℝhε:0 < εh:∀ (x_1 : ℤ), 0 ≤ x_1 → ∃ x_2, 0 ≤ x_2 ∧ x_1 ≤ x_2 ∧ ε < dist (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (x x_2.toNat) else 0 else 0) (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (y x_2.toNat) else 0 else 0)E:Set ℕ := {n | ¬Real.Close _fvar.258344 (@_fvar.19113 (@_fvar.201524 n)) (@_fvar.19113 (@_fvar.201542 n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth _fvar.258347hmono:StrictMono nhmem:∀ (j : ℕ), n j ∈ Ehsep:∀ (j : ℕ), |f (x (n j)) - f (y (n j))| > εhxmem:∀ (j : ℕ), x (n j) ∈ Set.Icc a bhymem:∀ (j : ℕ), y (n j) ∈ Set.Icc a bhclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)j:ℕ → ℕhj:StrictMono jL:ℝhL:L ∈ Set.Icc a bhconv:Tendsto (fun j_1 => x (n (j j_1))) atTop (nhds L)hcont:ContinuousWithinAt f (Set.Icc a b) Lhconv':Tendsto (fun n_1 => f (x (n (j n_1)))) atTop (nhds (f L))⊢ False replace hequiv : atTop.Tendsto (fun k ↦ x (n (j k)) - y (n (j k))) (nhds 0) := a:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)⊢ UniformContinuousOn f (Set.Icc a b) a:ℝb:ℝf:ℝ → ℝx:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a by:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:Tendsto (fun n => (↑x).seq n - (↑y).seq n) atTop (nhds 0)ε:ℝhε:0 < εh:∀ (x_1 : ℤ), 0 ≤ x_1 → ∃ x_2, 0 ≤ x_2 ∧ x_1 ≤ x_2 ∧ ε < dist (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (x x_2.toNat) else 0 else 0) (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (y x_2.toNat) else 0 else 0)E:Set ℕ := {n | ¬Real.Close _fvar.258344 (@_fvar.19113 (@_fvar.201524 n)) (@_fvar.19113 (@_fvar.201542 n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth _fvar.258347hmono:StrictMono nhmem:∀ (j : ℕ), n j ∈ Ehsep:∀ (j : ℕ), |f (x (n j)) - f (y (n j))| > εhxmem:∀ (j : ℕ), x (n j) ∈ Set.Icc a bhymem:∀ (j : ℕ), y (n j) ∈ Set.Icc a bhclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)j:ℕ → ℕhj:StrictMono jL:ℝhL:L ∈ Set.Icc a bhconv:Tendsto (fun j_1 => x (n (j j_1))) atTop (nhds L)hcont:ContinuousWithinAt f (Set.Icc a b) Lhconv':Tendsto (fun n_1 => f (x (n (j n_1)))) atTop (nhds (f L))hj':Tendsto j atTop atTop⊢ Tendsto (fun k => x (n (j k)) - y (n (j k))) atTop (nhds 0) a:ℝb:ℝf:ℝ → ℝx:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a by:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:Tendsto (fun n => (↑x).seq n - (↑y).seq n) atTop (nhds 0)ε:ℝhε:0 < εh:∀ (x_1 : ℤ), 0 ≤ x_1 → ∃ x_2, 0 ≤ x_2 ∧ x_1 ≤ x_2 ∧ ε < dist (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (x x_2.toNat) else 0 else 0) (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (y x_2.toNat) else 0 else 0)E:Set ℕ := {n | ¬Real.Close _fvar.258344 (@_fvar.19113 (@_fvar.201524 n)) (@_fvar.19113 (@_fvar.201542 n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth _fvar.258347hmono:StrictMono nhmem:∀ (j : ℕ), n j ∈ Ehsep:∀ (j : ℕ), |f (x (n j)) - f (y (n j))| > εhxmem:∀ (j : ℕ), x (n j) ∈ Set.Icc a bhymem:∀ (j : ℕ), y (n j) ∈ Set.Icc a bhclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)j:ℕ → ℕhj:StrictMono jL:ℝhL:L ∈ Set.Icc a bhconv:Tendsto (fun j_1 => x (n (j j_1))) atTop (nhds L)hcont:ContinuousWithinAt f (Set.Icc a b) Lhconv':Tendsto (fun n_1 => f (x (n (j n_1)))) atTop (nhds (f L))hj':Tendsto j atTop atTophn':Tendsto n atTop atTop⊢ Tendsto (fun k => x (n (j k)) - y (n (j k))) atTop (nhds 0) a:ℝb:ℝf:ℝ → ℝx:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a by:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:Tendsto (fun n => (↑x).seq n - (↑y).seq n) atTop (nhds 0)ε:ℝhε:0 < εh:∀ (x_1 : ℤ), 0 ≤ x_1 → ∃ x_2, 0 ≤ x_2 ∧ x_1 ≤ x_2 ∧ ε < dist (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (x x_2.toNat) else 0 else 0) (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (y x_2.toNat) else 0 else 0)E:Set ℕ := {n | ¬Real.Close _fvar.258344 (@_fvar.19113 (@_fvar.201524 n)) (@_fvar.19113 (@_fvar.201542 n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth _fvar.258347hmono:StrictMono nhmem:∀ (j : ℕ), n j ∈ Ehsep:∀ (j : ℕ), |f (x (n j)) - f (y (n j))| > εhxmem:∀ (j : ℕ), x (n j) ∈ Set.Icc a bhymem:∀ (j : ℕ), y (n j) ∈ Set.Icc a bhclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)j:ℕ → ℕhj:StrictMono jL:ℝhL:L ∈ Set.Icc a bhconv:Tendsto (fun j_1 => x (n (j j_1))) atTop (nhds L)hcont:ContinuousWithinAt f (Set.Icc a b) Lhconv':Tendsto (fun n_1 => f (x (n (j n_1)))) atTop (nhds (f L))hj':Tendsto j atTop atTophn':Tendsto n atTop atTophcoe:Tendsto Nat.cast atTop atTop⊢ Tendsto (fun k => x (n (j k)) - y (n (j k))) atTop (nhds 0) All goals completed! 🐙 have hyconv : atTop.Tendsto (fun k ↦ y (n (j k))) (nhds L) := a:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)⊢ UniformContinuousOn f (Set.Icc a b) a:ℝb:ℝf:ℝ → ℝx:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a by:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Icc a bε:ℝhε:0 < εh:∀ (x_1 : ℤ), 0 ≤ x_1 → ∃ x_2, 0 ≤ x_2 ∧ x_1 ≤ x_2 ∧ ε < dist (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (x x_2.toNat) else 0 else 0) (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (y x_2.toNat) else 0 else 0)E:Set ℕ := {n | ¬Real.Close _fvar.258344 (@_fvar.19113 (@_fvar.201524 n)) (@_fvar.19113 (@_fvar.201542 n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth _fvar.258347hmono:StrictMono nhmem:∀ (j : ℕ), n j ∈ Ehsep:∀ (j : ℕ), |f (x (n j)) - f (y (n j))| > εhxmem:∀ (j : ℕ), x (n j) ∈ Set.Icc a bhymem:∀ (j : ℕ), y (n j) ∈ Set.Icc a bhclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)j:ℕ → ℕhj:StrictMono jL:ℝhL:L ∈ Set.Icc a bhconv:Tendsto (fun j_1 => x (n (j j_1))) atTop (nhds L)hcont:ContinuousWithinAt f (Set.Icc a b) Lhconv':Tendsto (fun n_1 => f (x (n (j n_1)))) atTop (nhds (f L))hequiv:Tendsto (fun k => @_fvar.201524 (@_fvar.258350 (@_fvar.258358 k)) - @_fvar.201542 (@_fvar.258350 (@_fvar.258358 k))) atTop (nhds 0) := ?_mvar.258657k:ℕ⊢ y (n (j k)) = x (n (j k)) - (x (n (j k)) - y (n (j k)))a:ℝb:ℝf:ℝ → ℝx:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a by:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Icc a bε:ℝhε:0 < εh:∀ (x_1 : ℤ), 0 ≤ x_1 → ∃ x_2, 0 ≤ x_2 ∧ x_1 ≤ x_2 ∧ ε < dist (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (x x_2.toNat) else 0 else 0) (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (y x_2.toNat) else 0 else 0)E:Set ℕ := {n | ¬Real.Close _fvar.258344 (@_fvar.19113 (@_fvar.201524 n)) (@_fvar.19113 (@_fvar.201542 n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth _fvar.258347hmono:StrictMono nhmem:∀ (j : ℕ), n j ∈ Ehsep:∀ (j : ℕ), |f (x (n j)) - f (y (n j))| > εhxmem:∀ (j : ℕ), x (n j) ∈ Set.Icc a bhymem:∀ (j : ℕ), y (n j) ∈ Set.Icc a bhclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)j:ℕ → ℕhj:StrictMono jL:ℝhL:L ∈ Set.Icc a bhconv:Tendsto (fun j_1 => x (n (j j_1))) atTop (nhds L)hcont:ContinuousWithinAt f (Set.Icc a b) Lhconv':Tendsto (fun n_1 => f (x (n (j n_1)))) atTop (nhds (f L))hequiv:Tendsto (fun k => @_fvar.201524 (@_fvar.258350 (@_fvar.258358 k)) - @_fvar.201542 (@_fvar.258350 (@_fvar.258358 k))) atTop (nhds 0) := ?_mvar.258657⊢ L = L - 0 a:ℝb:ℝf:ℝ → ℝx:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a by:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Icc a bε:ℝhε:0 < εh:∀ (x_1 : ℤ), 0 ≤ x_1 → ∃ x_2, 0 ≤ x_2 ∧ x_1 ≤ x_2 ∧ ε < dist (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (x x_2.toNat) else 0 else 0) (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (y x_2.toNat) else 0 else 0)E:Set ℕ := {n | ¬Real.Close _fvar.258344 (@_fvar.19113 (@_fvar.201524 n)) (@_fvar.19113 (@_fvar.201542 n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth _fvar.258347hmono:StrictMono nhmem:∀ (j : ℕ), n j ∈ Ehsep:∀ (j : ℕ), |f (x (n j)) - f (y (n j))| > εhxmem:∀ (j : ℕ), x (n j) ∈ Set.Icc a bhymem:∀ (j : ℕ), y (n j) ∈ Set.Icc a bhclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)j:ℕ → ℕhj:StrictMono jL:ℝhL:L ∈ Set.Icc a bhconv:Tendsto (fun j_1 => x (n (j j_1))) atTop (nhds L)hcont:ContinuousWithinAt f (Set.Icc a b) Lhconv':Tendsto (fun n_1 => f (x (n (j n_1)))) atTop (nhds (f L))hequiv:Tendsto (fun k => @_fvar.201524 (@_fvar.258350 (@_fvar.258358 k)) - @_fvar.201542 (@_fvar.258350 (@_fvar.258358 k))) atTop (nhds 0) := ?_mvar.258657k:ℕ⊢ y (n (j k)) = x (n (j k)) - (x (n (j k)) - y (n (j k))) All goals completed! 🐙 All goals completed! 🐙 a:ℝb:ℝf:ℝ → ℝx:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a by:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Icc a bε:ℝhε:0 < εh:∀ (x_1 : ℤ), 0 ≤ x_1 → ∃ x_2, 0 ≤ x_2 ∧ x_1 ≤ x_2 ∧ ε < dist (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (x x_2.toNat) else 0 else 0) (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (y x_2.toNat) else 0 else 0)E:Set ℕ := {n | ¬Real.Close _fvar.258344 (@_fvar.19113 (@_fvar.201524 n)) (@_fvar.19113 (@_fvar.201542 n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth _fvar.258347hmono:StrictMono nhmem:∀ (j : ℕ), n j ∈ Ehsep:∀ (j : ℕ), |f (x (n j)) - f (y (n j))| > εhxmem:∀ (j : ℕ), x (n j) ∈ Set.Icc a bhymem:∀ (j : ℕ), y (n j) ∈ Set.Icc a bhclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)j:ℕ → ℕhj:StrictMono jL:ℝhL:L ∈ Set.Icc a bhconv:Tendsto (fun j_1 => x (n (j j_1))) atTop (nhds L)hcont:ContinuousWithinAt f (Set.Icc a b) Lhconv':Tendsto (fun n_1 => f (x (n (j n_1)))) atTop (nhds (f L))hequiv:Tendsto (fun k => @_fvar.201524 (@_fvar.258350 (@_fvar.258358 k)) - @_fvar.201542 (@_fvar.258350 (@_fvar.258358 k))) atTop (nhds 0) := ?_mvar.258657hyconv:?_mvar.344363 := Tendsto.comp_of_continuous _fvar.258361 _fvar.258363 (fun k => @_fvar.258355 (@_fvar.258358 k)) _fvar.342055⊢ False have : atTop.Tendsto (fun k ↦ f (x (n (j k))) - f (y (n (j k)))) (nhds 0) := a:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)⊢ UniformContinuousOn f (Set.Icc a b) a:ℝb:ℝf:ℝ → ℝx:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a by:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Icc a bε:ℝhε:0 < εh:∀ (x_1 : ℤ), 0 ≤ x_1 → ∃ x_2, 0 ≤ x_2 ∧ x_1 ≤ x_2 ∧ ε < dist (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (x x_2.toNat) else 0 else 0) (if 0 ≤ x_2 ∧ x_1 ≤ x_2 then if 0 ≤ x_2 then f (y x_2.toNat) else 0 else 0)E:Set ℕ := {n | ¬Real.Close _fvar.258344 (@_fvar.19113 (@_fvar.201524 n)) (@_fvar.19113 (@_fvar.201542 n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth _fvar.258347hmono:StrictMono nhmem:∀ (j : ℕ), n j ∈ Ehsep:∀ (j : ℕ), |f (x (n j)) - f (y (n j))| > εhxmem:∀ (j : ℕ), x (n j) ∈ Set.Icc a bhymem:∀ (j : ℕ), y (n j) ∈ Set.Icc a bhclosed:IsClosed (Set.Icc a b)hbounded:Bornology.IsBounded (Set.Icc a b)j:ℕ → ℕhj:StrictMono jL:ℝhL:L ∈ Set.Icc a bhconv:Tendsto (fun j_1 => x (n (j j_1))) atTop (nhds L)hcont:ContinuousWithinAt f (Set.Icc a b) Lhconv':Tendsto (fun n_1 => f (x (n (j n_1)))) atTop (nhds (f L))hequiv:Tendsto (fun k => @_fvar.201524 (@_fvar.258350 (@_fvar.258358 k)) - @_fvar.201542 (@_fvar.258350 (@_fvar.258358 k))) atTop (nhds 0) := ?_mvar.258657hyconv:?_mvar.344363 := Tendsto.comp_of_continuous _fvar.258361 _fvar.258363 (fun k => @_fvar.258355 (@_fvar.258358 k)) _fvar.342055⊢ 0 = f L - f L; All goals completed! 🐙 All goals completed! 🐙

Exercise 9.9.6

theorem declaration uses 'sorry'UniformContinuousOn.comp {X Y: Set ℝ} {f g:ℝ → ℝ} (hf: UniformContinuousOn f X) (hg: UniformContinuousOn g Y) (hrange: f '' X ⊆ Y) : UniformContinuousOn (g ∘ f) X := X:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhf:UniformContinuousOn f Xhg:UniformContinuousOn g Yhrange:f '' X ⊆ Y⊢ UniformContinuousOn (g ∘ f) X All goals completed! 🐙
end Chapter9