Analysis
9.9. Uniform continuity

Imports

import Mathlib.Tactic
import Analysis.Section_6_1
import Mathlib.Data.Nat.Nth
import Analysis.Section_9_6

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:

API for Mathlib's UniformContinuousOn.
Continuous functions on compact intervals are uniformly continuous.

              open Chapter6 Filternamespace Chapter9declaration uses `sorry`example : ContinuousOn (fun x:ℝ ↦ 1/x) (.Ioo 0 2) := by⊢ ContinuousOn (fun x ↦ 1 / x) (Set.Ioo 0 2)
  sorryAll goals completed! 🐙declaration uses `sorry`example : ¬ BddOn (fun x:ℝ ↦ 1/x) (.Ioo 0 2) := by⊢ ¬BddOn (fun x ↦ 1 / x) (Set.Ioo 0 2)
  sorryAll 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₀| ≤ ε := byx:ℝ⊢ let f := fun x ↦ 1 / x;
let ε := 0.1;
let x₀ := 1;
let δ := 1 / 11;
|x - x₀| ≤ δ → |f x - f x₀| ≤ ε
  extract_lets f ε x₀ δx:ℝf:ℝ → ℝ := fun x ↦ 1 / xε:ℝ := 0.1x₀:ℝ := 1δ:ℝ := 1 / 11⊢ |x - x₀| ≤ δ → |f x - f x₀| ≤ ε
  sorryAll 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₀| ≤ ε := byx:ℝ⊢ let f := fun x ↦ 1 / x;
let ε := 0.1;
let x₀ := 0.1;
let δ := 1 / 1010;
|x - x₀| ≤ δ → |f x - f x₀| ≤ ε
  extract_lets -merge 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₀`
  sorryAll 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₀| ≤ ε := byx:ℝ⊢ let g := fun x ↦ 2 * x;
let ε := 0.1;
let x₀ := 1;
let δ := 5e-2;
|x - x₀| ≤ δ → |g x - g x₀| ≤ ε
  extract_lets g ε x₀ δx:ℝg:ℝ → ℝ := fun x ↦ 2 * xε:ℝ := 0.1x₀:ℝ := 1δ:ℝ := 5e-2⊢ |x - x₀| ≤ δ → |g x - g x₀| ≤ ε
  sorryAll 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₀| ≤ ε := byx₀:ℝx:ℝ⊢ let g := fun x ↦ 2 * x;
let ε := 0.1;
let δ := 5e-2;
|x - x₀| ≤ δ → |g x - g x₀| ≤ ε
  extract_lets g ε δx₀:ℝx:ℝg:ℝ → ℝ := fun x ↦ 2 * xε:ℝ := 0.1δ:ℝ := 5e-2⊢ |x - x₀| ≤ δ → |g x - g x₀| ≤ ε
  sorryAll goals completed! 🐙

Definition 9.9.2. Here we use the Mathlib term UniformContinuousOn

theorem UniformContinuousOn.iff (f: ℝ → ℝ) (X:Set ℝ) : UniformContinuousOn f X  ↔
  ∀ ε > (0:ℝ), ∃ δ > (0:ℝ), ∀ x₀ ∈ X, ∀ x ∈ X, δ.Close x x₀ → ε.Close (f x) (f x₀) := byf:ℝ → ℝX:Set ℝ⊢ UniformContinuousOn f X ↔ ∀ ε > 0, ∃ δ > 0, ∀ x₀ ∈ X, ∀ x ∈ X, δ.Close x x₀ → ε.Close (f x) (f x₀)
  simp_rw [f:ℝ → ℝX:Set ℝ⊢ UniformContinuousOn f X ↔ ∀ ε > 0, ∃ δ > 0, ∀ x₀ ∈ X, ∀ x ∈ X, δ.Close x x₀ → ε.Close (f x) (f x₀)Metric.uniformContinuousOn_iff_le, Real.Close]
  grindAll goals completed! 🐙

              theorem declaration uses `sorry`ContinuousOn.ofUniformContinuousOn {X:Set ℝ} (f: ℝ → ℝ) (hf: UniformContinuousOn f X) :
  ContinuousOn f X := byX:Set ℝf:ℝ → ℝhf:UniformContinuousOn f X⊢ ContinuousOn f X
  sorryAll goals completed! 🐙declaration uses `sorry`example : ¬ UniformContinuousOn (fun x:ℝ ↦ 1/x) (Set.Ioo 0 2) := by⊢ ¬UniformContinuousOn (fun x ↦ 1 / x) (Set.Ioo 0 2)
  sorryAll goals completed! 🐙end Chapter9

Definition 9.9.5. This is similar but not identical to Real.CloseSeq 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 := bya:Sequenceb:Sequence⊢ a.equiv b ↔ ∀ ε > 0, (↑ε).EventuallyCloseSeqs a b
  sorryAll 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) := bya:Sequenceb:Sequence⊢ a.equiv b ↔ Tendsto (fun n ↦ a.seq n - b.seq n) atTop (nhds 0)
  sorryAll 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) := byX:Set ℝf:ℝ → ℝ⊢ UniformContinuousOn f X ↔
  ∀ (x y : ℕ → ℝ), (∀ (n : ℕ), x n ∈ X) → (∀ (n : ℕ), y n ∈ X) → (↑x).equiv ↑y → (↑(f ∘ x)).equiv ↑(f ∘ y)
  sorryAll 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) := byx₀:ℝx:ℕ → ℝ⊢ Tendsto x atTop (nhds x₀) ↔ (↑x).equiv ↑fun n ↦ x₀
  sorryAll 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) := by⊢ (↑fun n ↦ 1 / (↑n + 1)).equiv ↑fun n ↦ 1 / (2 * (↑n + 1)) sorryAll goals completed! 🐙declaration uses `sorry`example (n:ℕ) : 1/(n+1:ℝ) ∈ Set.Ioo 0 2 := byn:ℕ⊢ 1 / (↑n + 1) ∈ Set.Ioo 0 2 sorryAll goals completed! 🐙declaration uses `sorry`example (n:ℕ) : 1/(2*(n+1):ℝ) ∈ Set.Ioo 0 2 := byn:ℕ⊢ 1 / (2 * (↑n + 1)) ∈ Set.Ioo 0 2 sorryAll 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) := by⊢ ¬(↑fun n ↦ f_9_9_10 (1 / (↑n + 1))).equiv ↑fun n ↦ f_9_9_10 (1 / (2 * (↑n + 1))) sorryAll goals completed! 🐙declaration uses `sorry`example : ¬ UniformContinuousOn f_9_9_10 (.Ioo 0 2) := by⊢ ¬UniformContinuousOn f_9_9_10 (Set.Ioo 0 2)
  sorryAll 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) := by⊢ (↑fun n ↦ ↑n + 1).equiv ↑fun n ↦ ↑n + 1 + 1 / (↑n + 1)
  sorryAll 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) := by⊢ ¬(↑fun n ↦ f_9_9_11 (↑n + 1)).equiv ↑fun n ↦ f_9_9_11 (↑n + 1 + 1 / (↑n + 1))
  sorryAll goals completed! 🐙declaration uses `sorry`example : ¬ UniformContinuousOn f_9_9_11 .univ := by⊢ ¬UniformContinuousOn f_9_9_11 Set.univ
  sorryAll 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 := byX:Set ℝf:ℝ → ℝhf:UniformContinuousOn f Xx:ℕ → ℝhx:(↑x).IsCauchyhmem:∀ (n : ℕ), x n ∈ X⊢ (↑(f ∘ x)).IsCauchy
  sorryAll goals completed! 🐙

              /-- Example 9.9.13 -/
declaration uses `sorry`example : ((fun n:ℕ ↦ 1/(n+1:ℝ)):Sequence).IsCauchy := by⊢ (↑fun n ↦ 1 / (↑n + 1)).IsCauchy
  sorryAll goals completed! 🐙declaration uses `sorry`example (n:ℕ) : 1/(n+1:ℝ) ∈ Set.Ioo 0 2 := byn:ℕ⊢ 1 / (↑n + 1) ∈ Set.Ioo 0 2
  sorryAll goals completed! 🐙declaration uses `sorry`example : ¬ ((fun n:ℕ ↦ f_9_9_10 (1/(n+1:ℝ))):Sequence).IsCauchy := by⊢ ¬(↑fun n ↦ f_9_9_10 (1 / (↑n + 1))).IsCauchy
  sorryAll goals completed! 🐙declaration uses `sorry`example : ¬ UniformContinuousOn f_9_9_10 (Set.Ioo 0 2) := by⊢ ¬UniformContinuousOn f_9_9_10 (Set.Ioo 0 2)
  sorryAll 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) := byX:Set ℝf:ℝ → ℝhf:UniformContinuousOn f Xx₀:ℝhx₀:AdherentPt x₀ X⊢ ∃ L, Tendsto f (nhdsWithin x₀ X) (nhds L)
  sorryAll 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) := byE:Set ℝX:Set ℝf:ℝ → ℝhf:UniformContinuousOn f XhEX:E ⊆ XhE:Bornology.IsBounded E⊢ Bornology.IsBounded (f '' E)
  sorryAll 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) := bya:ℝ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.
  by_contra ha:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)h:¬UniformContinuousOn f (Set.Icc a b)⊢ False; rw [iff_preserves_equiv] at ha:ℝ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
  simp [-Set.mem_Icc] at ha:ℝ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
  choose x hx y hy hequiv ε hε h using ha:ℝ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
  set E : Set ℕ := {n | ¬ ε.Close (f (x n)) (f (y n)) }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 | ¬ε.Close (f (x n)) (f (y n))}⊢ False
  have hE : Infinite E := bya:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)⊢ UniformContinuousOn f (Set.Icc a b)
    rw [←not_finite_iff_infinite]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 | ¬ε.Close (f (x n)) (f (y n))}⊢ ¬Finite ↑E
    by_contra! thisa:ℝ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 | ¬ε.Close (f (x n)) (f (y n))}this:Finite ↑E⊢ False
    replace : ε.EventuallyCloseSeqs (fun n ↦ f (x n):Sequence) (fun n ↦ f (y n):Sequence) := bya:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)⊢ UniformContinuousOn f (Set.Icc a b)
      sorryAll goals completed! 🐙
    sorryAll goals completed! 🐙
  observe : Countable Ea:ℝ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 | ¬ε.Close (f (x n)) (f (y n))}hE:Infinite ↑Ethis:Countable ↑E⊢ False
  set n : ℕ → ℕ := Nat.nth Ea:ℝ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 | ¬ε.Close (f (x n)) (f (y n))}hE:Infinite ↑Ethis:Countable ↑En:ℕ → ℕ := Nat.nth E⊢ False
  rw [Set.infinite_coe_iff] at hEa:ℝ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 | ¬ε.Close (f (x n)) (f (y n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth E⊢ False
  have hmono : StrictMono n := bya:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)⊢ UniformContinuousOn f (Set.Icc a b) apply_rules [Nat.nth_strictMono]All goals completed! 🐙
  have hmem (j:ℕ) : n j ∈ E := j.nth_mem_of_infinite hEa:ℝ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 | ¬ε.Close (f (x n)) (f (y n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth Ehmono:StrictMono nhmem:∀ (j : ℕ), n j ∈ E⊢ False
  have hsep (j:ℕ) : |f (x (n j)) - f (y (n j))| > ε := bya:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)⊢ UniformContinuousOn f (Set.Icc a b)
    specialize hmem ja:ℝ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 | ¬ε.Close (f (x n)) (f (y n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth Ehmono:StrictMono nj:ℕhmem:n j ∈ E⊢ |f (x (n j)) - f (y (n j))| > ε
    simpa [E, Real.Close, Real.dist_eq] using hmemAll goals completed! 🐙
  observe hxmem : ∀ j, x (n j) ∈ Set.Icc a ba:ℝ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 | ¬ε.Close (f (x n)) (f (y n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth Ehmono:StrictMono nhmem:∀ (j : ℕ), n j ∈ Ehsep:∀ (j : ℕ), |f (x (n j)) - f (y (n j))| > εhxmem:∀ (j : ℕ), x (n j) ∈ Set.Icc a b⊢ False
  observe hymem : ∀ j, y (n j) ∈ Set.Icc a ba:ℝ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 | ¬ε.Close (f (x n)) (f (y n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth Ehmono: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 b⊢ False
  observe hclosed : IsClosed (.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 | ¬ε.Close (f (x n)) (f (y n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth Ehmono: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)⊢ False
  observe hbounded : Bornology.IsBounded (.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 | ¬ε.Close (f (x n)) (f (y n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth Ehmono: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)⊢ False
  have ⟨ j, hj, ⟨ L, hL, hconv⟩ ⟩ := (Heine_Borel (.Icc a b)).mp ⟨ hclosed, hbounded ⟩ _ hxmema:ℝ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 | ¬ε.Close (f (x n)) (f (y n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth Ehmono: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)⊢ False
  replace hcont := ContinuousOn.continuousWithinAt hcont hLa:ℝ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 | ¬ε.Close (f (x n)) (f (y n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth Ehmono: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) L⊢ False
  have hconv' := hconv.comp_of_continuous hcont (fun k ↦ hxmem (j k))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 | ¬ε.Close (f (x n)) (f (y n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth Ehmono: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
  rw [Sequence.equiv_iff] at hequiva:ℝ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 | ¬ε.Close (f (x n)) (f (y n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth Ehmono: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) := bya:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)⊢ UniformContinuousOn f (Set.Icc a b)
    observe hj' : atTop.Tendsto j .atTopa:ℝ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 | ¬ε.Close (f (x n)) (f (y n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth Ehmono: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)
    observe hn' : atTop.Tendsto n .atTopa:ℝ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 | ¬ε.Close (f (x n)) (f (y n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth Ehmono: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)
    observe hcoe : atTop.Tendsto (fun n:ℕ ↦ (n:ℤ)) .atTopa:ℝ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 | ¬ε.Close (f (x n)) (f (y n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth Ehmono: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)
    exact hequiv.comp (hcoe.comp (hn'.comp hj'))All goals completed! 🐙
  have hyconv : atTop.Tendsto (fun k ↦ y (n (j k))) (nhds L) := bya:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)⊢ UniformContinuousOn f (Set.Icc a b)
    convert hconv.sub hequiv with kh.e'_3.ha:ℝ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 | ¬ε.Close (f (x n)) (f (y n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth Ehmono: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 ↦ x (n (j k)) - y (n (j k))) atTop (nhds 0)k:ℕ⊢ y (n (j k)) = x (n (j k)) - (x (n (j k)) - y (n (j k)))h.e'_5.h.e'_3a:ℝ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 | ¬ε.Close (f (x n)) (f (y n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth Ehmono: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 ↦ x (n (j k)) - y (n (j k))) atTop (nhds 0)⊢ L = L - 0
    .h.e'_3.ha:ℝ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 | ¬ε.Close (f (x n)) (f (y n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth Ehmono: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 ↦ x (n (j k)) - y (n (j k))) atTop (nhds 0)k:ℕ⊢ y (n (j k)) = x (n (j k)) - (x (n (j k)) - y (n (j k))) abelAll goals completed! 🐙
    simpAll goals completed! 🐙
  replace hyconv := hyconv.comp_of_continuous hcont (fun k ↦ hymem (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 | ¬ε.Close (f (x n)) (f (y n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth Ehmono: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 ↦ x (n (j k)) - y (n (j k))) atTop (nhds 0)hyconv:Tendsto (fun n_1 ↦ f (y (n (j n_1)))) atTop (nhds (f L))⊢ False
  have : atTop.Tendsto (fun k ↦ f (x (n (j k))) - f (y (n (j k)))) (nhds 0) := bya:ℝb:ℝf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)⊢ UniformContinuousOn f (Set.Icc a b)
    convert hconv'.sub hyconvh.e'_5.h.e'_3a:ℝ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 | ¬ε.Close (f (x n)) (f (y n))}hE:E.Infinitethis:Countable ↑En:ℕ → ℕ := Nat.nth Ehmono: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 ↦ x (n (j k)) - y (n (j k))) atTop (nhds 0)hyconv:Tendsto (fun n_1 ↦ f (y (n (j n_1)))) atTop (nhds (f L))⊢ 0 = f L - f L; simpAll goals completed! 🐙
  sorryAll 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 := byX:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhf:UniformContinuousOn f Xhg:UniformContinuousOn g Yhrange:f '' X ⊆ Y⊢ UniformContinuousOn (g ∘ f) X
  sorryAll goals completed! 🐙

end Chapter9