Аналіз I, Глава 9.9
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
UniformContinousOn
-
Continuous functions on compact intervls are uniformly continuous
open Chapter6
namespace Chapter9
example : ContinuousOn (fun x:ℝ ↦ 1/x) (Set.Icc 0 2) := ⊢ ContinuousOn (fun x => 1 / x) (Set.Icc 0 2)
All goals completed! 🐙
example : ¬ BddOn (fun x:ℝ ↦ 1/x) (Set.Icc 0 2) := ⊢ ¬BddOn (fun x => 1 / x) (Set.Icc 0 2)
All goals completed! 🐙
Приклад 9.9.1
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₀| ≤ ε
All goals completed! 🐙
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₀| ≤ ε
All goals completed! 🐙
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₀| ≤ ε
All goals completed! 🐙
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₀| ≤ ε
All goals completed! 🐙
Визначення 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₀) := 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₀) ≤ ε
f:ℝ → ℝX:Set ℝ⊢ ∀ (a : ℝ),
(a > 0 → ∃ δ > 0, ∀ x ∈ X, ∀ y ∈ X, dist x y ≤ δ → dist (f x) (f y) ≤ a) ↔
a > 0 → ∃ δ > 0, ∀ x₀ ∈ X, ∀ x ∈ X, dist x x₀ ≤ δ → dist (f x) (f x₀) ≤ a; 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₀) ≤ ε
f:ℝ → ℝX:Set ℝε:ℝ⊢ ε > 0 →
((∃ δ > 0, ∀ x ∈ X, ∀ y ∈ X, dist x y ≤ δ → dist (f x) (f y) ≤ ε) ↔
∃ δ > 0, ∀ x₀ ∈ X, ∀ x ∈ X, dist x x₀ ≤ δ → dist (f x) (f x₀) ≤ ε); f:ℝ → ℝX:Set ℝε:ℝhε:ε > 0⊢ (∃ δ > 0, ∀ x ∈ X, ∀ y ∈ X, dist x y ≤ δ → dist (f x) (f y) ≤ ε) ↔
∃ δ > 0, ∀ x₀ ∈ X, ∀ x ∈ X, dist x x₀ ≤ δ → dist (f x) (f x₀) ≤ ε
f:ℝ → ℝX:Set ℝε:ℝhε:ε > 0⊢ ∀ (a : ℝ),
(a > 0 ∧ ∀ x ∈ X, ∀ y ∈ X, dist x y ≤ a → dist (f x) (f y) ≤ ε) ↔
a > 0 ∧ ∀ x₀ ∈ X, ∀ x ∈ X, dist x x₀ ≤ a → dist (f x) (f x₀) ≤ ε; f:ℝ → ℝX:Set ℝε:ℝhε:ε > 0δ:ℝ⊢ (δ > 0 ∧ ∀ x ∈ X, ∀ y ∈ X, dist x y ≤ δ → dist (f x) (f y) ≤ ε) ↔
δ > 0 ∧ ∀ x₀ ∈ X, ∀ x ∈ X, dist x x₀ ≤ δ → dist (f x) (f x₀) ≤ ε
f:ℝ → ℝX:Set ℝε:ℝhε:ε > 0δ:ℝ⊢ δ > 0 →
((∀ x ∈ X, ∀ y ∈ X, dist x y ≤ δ → dist (f x) (f y) ≤ ε) ↔ ∀ x₀ ∈ X, ∀ x ∈ X, dist x x₀ ≤ δ → dist (f x) (f x₀) ≤ ε); f:ℝ → ℝX:Set ℝε:ℝhε:ε > 0δ:ℝhδ:δ > 0⊢ (∀ x ∈ X, ∀ y ∈ X, dist x y ≤ δ → dist (f x) (f y) ≤ ε) ↔ ∀ x₀ ∈ X, ∀ x ∈ X, dist x x₀ ≤ δ → dist (f x) (f x₀) ≤ ε
f:ℝ → ℝX:Set ℝε:ℝhε:ε > 0δ:ℝhδ:δ > 0⊢ (∀ x ∈ X, ∀ y ∈ X, dist x y ≤ δ → dist (f x) (f y) ≤ ε) → ∀ x₀ ∈ X, ∀ x ∈ X, dist x x₀ ≤ δ → dist (f x) (f x₀) ≤ εf:ℝ → ℝX:Set ℝε:ℝhε:ε > 0δ:ℝhδ:δ > 0⊢ (∀ x₀ ∈ X, ∀ x ∈ X, dist x x₀ ≤ δ → dist (f x) (f x₀) ≤ ε) → ∀ x ∈ X, ∀ y ∈ X, dist x y ≤ δ → dist (f x) (f y) ≤ ε
f:ℝ → ℝX:Set ℝε:ℝhε:ε > 0δ:ℝhδ:δ > 0⊢ (∀ x ∈ X, ∀ y ∈ X, dist x y ≤ δ → dist (f x) (f y) ≤ ε) → ∀ x₀ ∈ X, ∀ x ∈ X, dist x x₀ ≤ δ → dist (f x) (f x₀) ≤ ε All goals completed! 🐙
All goals completed! 🐙
theorem 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! 🐙
example : ¬ UniformContinuousOn (fun x:ℝ ↦ 1/x) (Set.Icc 0 2) := ⊢ ¬UniformContinuousOn (fun x => 1 / x) (Set.Icc 0 2)
All goals completed! 🐙
end Chapter9
Визначення 9.9.5. This is similar but not identical to Real.close_seq
from Section 6.1.
abbrev Real.close_seqs (ε:ℝ) (a b: Chapter6.Sequence) : Prop :=
(a.m = b.m) ∧ ∀ n ≥ a.m, ε.close (a n) (b n)
abbrev Real.eventually_close_seqs (ε:ℝ) (a b: Chapter6.Sequence) : Prop :=
∃ N ≥ a.m, ε.close_seqs (a.from N) (b.from N)
abbrev Chapter6.Sequence.equiv (a b: Sequence) : Prop :=
∀ ε > (0:ℝ), ε.eventually_close_seqs a b
Ремарка 9.9.6
theorem Chapter6.Sequence.equiv_iff_rat (a b: Sequence) :
Sequence.equiv a b ↔ ∀ ε > (0:ℚ), (ε:ℝ).eventually_close_seqs a b := a:Sequenceb:Sequence⊢ a.equiv b ↔ ∀ ε > 0, (↑ε).eventually_close_seqs a b
All goals completed! 🐙
Лема 9.9.7 / Вправа 9.9.1
theorem Chapter6.Sequence.equiv_iff (a b: Sequence) :
Sequence.equiv a b ↔ Filter.Tendsto (fun n ↦ a n - b n) Filter.atTop (nhds 0) := a:Sequenceb:Sequence⊢ a.equiv b ↔ Filter.Tendsto (fun n => a.seq n - b.seq n) Filter.atTop (nhds 0)
All goals completed! 🐙
namespace Chapter9
Твердження 9.9.8 / Вправа 9.9.2
theorem UniformContinuousOn.iff_preserves_equiv {X:Set ℝ} (f: ℝ → ℝ) :
UniformContinuousOn f X ↔
∀ x y: ℕ → ℝ, (∀ n, x n ∈ X) → (∀ n, y n ∈ X) →
Sequence.equiv (x:Sequence) (y:Sequence) →
Sequence.equiv (f ∘ x:Sequence) (f ∘ y:Sequence) := X:Set ℝf:ℝ → ℝ⊢ UniformContinuousOn f X ↔
∀ (x y : ℕ → ℝ),
(∀ (n : ℕ), x n ∈ X) →
(∀ (n : ℕ), y n ∈ X) →
{ m := 0, seq := fun n => if n ≥ 0 then x n.toNat else 0, vanish := ⋯ }.equiv
{ m := 0, seq := fun n => if n ≥ 0 then y n.toNat else 0, vanish := ⋯ } →
{ m := 0, seq := fun n => if n ≥ 0 then (f ∘ x) n.toNat else 0, vanish := ⋯ }.equiv
{ m := 0, seq := fun n => if n ≥ 0 then (f ∘ y) n.toNat else 0, vanish := ⋯ }
All goals completed! 🐙
Ремарка 9.9.9
theorem Chapter6.Sequence.equiv_const (x₀: ℝ) (x:ℕ → ℝ) : Filter.Tendsto x Filter.atTop (nhds x₀) ↔
Sequence.equiv (x:Sequence) (fun n:ℕ ↦ x₀:Sequence) := x₀:ℝx:ℕ → ℝ⊢ Filter.Tendsto x Filter.atTop (nhds x₀) ↔
{ m := 0, seq := fun n => if n ≥ 0 then x n.toNat else 0, vanish := ⋯ }.equiv
{ m := 0, seq := fun n => if n ≥ 0 then (fun n => x₀) n.toNat else 0, vanish := ⋯ }
All goals completed! 🐙
example : Sequence.equiv (fun n:ℕ ↦ 1/(n+1:ℝ):Sequence) (fun n:ℕ ↦ 1/(2*(n+1):ℝ):Sequence) := ⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1)) n.toNat else 0, vanish := ⋯ }.equiv
{ m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (2 * (↑n + 1))) n.toNat else 0, vanish := ⋯ } All goals completed! 🐙
example (n:ℕ) : 1/(n+1:ℝ) ∈ Set.Ioo 0 2 := n:ℕ⊢ 1 / (↑n + 1) ∈ Set.Ioo 0 2 All goals completed! 🐙
example (n:ℕ) : 1/(2*(n+1):ℝ) ∈ Set.Ioo 0 2 := n:ℕ⊢ 1 / (2 * (↑n + 1)) ∈ Set.Ioo 0 2 All goals completed! 🐙
example : ¬ Sequence.equiv (fun n:ℕ ↦ f_9_9_10 (1/(n+1:ℝ)):Sequence) (fun n:ℕ ↦ f_9_9_10 (1/(2*(n+1):ℝ)):Sequence) := ⊢ ¬{ m := 0, seq := fun n => if n ≥ 0 then (fun n => f_9_9_10 (1 / (↑n + 1))) n.toNat else 0, vanish := ⋯ }.equiv
{ m := 0, seq := fun n => if n ≥ 0 then (fun n => f_9_9_10 (1 / (2 * (↑n + 1)))) n.toNat else 0, vanish := ⋯ } All goals completed! 🐙
example : ¬ UniformContinuousOn f_9_9_10 (Set.Ioo 0 2) := ⊢ ¬UniformContinuousOn f_9_9_10 (Set.Ioo 0 2)
All goals completed! 🐙
example : Sequence.equiv ((fun n:ℕ ↦ (n+1:ℝ)):Sequence) ((fun n:ℕ ↦ (n+1)+1/(n+1:ℝ)):Sequence) := ⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => ↑n + 1) n.toNat else 0, vanish := ⋯ }.equiv
{ m := 0, seq := fun n => if n ≥ 0 then (fun n => ↑n + 1 + 1 / (↑n + 1)) n.toNat else 0, vanish := ⋯ }
All goals completed! 🐙
example : ¬ Sequence.equiv ((fun n:ℕ ↦ f_9_9_11 (n+1:ℝ)):Sequence) ((fun n:ℕ ↦ f_9_9_11 ((n+1)+1/(n+1:ℝ))):Sequence) := ⊢ ¬{ m := 0, seq := fun n => if n ≥ 0 then (fun n => f_9_9_11 (↑n + 1)) n.toNat else 0, vanish := ⋯ }.equiv
{ m := 0, seq := fun n => if n ≥ 0 then (fun n => f_9_9_11 (↑n + 1 + 1 / (↑n + 1))) n.toNat else 0, vanish := ⋯ }
All goals completed! 🐙
example : ¬ UniformContinuousOn f_9_9_11 Set.univ := ⊢ ¬UniformContinuousOn f_9_9_11 Set.univ
All goals completed! 🐙
Твердження 9.9.12 / Вправа 9.9.3
theorem 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:{ m := 0, seq := fun n => if n ≥ 0 then x n.toNat else 0, vanish := ⋯ }.isCauchyhmem:∀ (n : ℕ), x n ∈ X⊢ { m := 0, seq := fun n => if n ≥ 0 then (f ∘ x) n.toNat else 0, vanish := ⋯ }.isCauchy
All goals completed! 🐙
Приклад 9.9.13
example : ((fun n:ℕ ↦ 1/(n+1:ℝ)):Sequence).isCauchy := ⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1 / (↑n + 1)) n.toNat else 0, vanish := ⋯ }.isCauchy
All goals completed! 🐙
example (n:ℕ) : 1/(n+1:ℝ) ∈ Set.Ioo 0 2 := n:ℕ⊢ 1 / (↑n + 1) ∈ Set.Ioo 0 2
All goals completed! 🐙
example : ¬ ((fun n:ℕ ↦ f_9_9_10 (1/(n+1:ℝ))):Sequence).isCauchy := ⊢ ¬{ m := 0, seq := fun n => if n ≥ 0 then (fun n => f_9_9_10 (1 / (↑n + 1))) n.toNat else 0, vanish := ⋯ }.isCauchy
All goals completed! 🐙
example : ¬ UniformContinuousOn f_9_9_10 (Set.Ioo 0 2) := ⊢ ¬UniformContinuousOn f_9_9_10 (Set.Ioo 0 2)
All goals completed! 🐙
Наслідок 9.9.14 / Вправа 9.9.4
theorem UniformContinuousOn.limit_at_adherent {X:Set ℝ} (f: ℝ → ℝ)
(hf: UniformContinuousOn f X) {x₀:ℝ} (hx₀: AdherentPt x₀ X) :
∃ L:ℝ, Filter.Tendsto f (nhds x₀ ⊓ Filter.principal X) (nhds L) := X:Set ℝf:ℝ → ℝhf:UniformContinuousOn f Xx₀:ℝhx₀:AdherentPt x₀ X⊢ ∃ L, Filter.Tendsto f (nhds x₀ ⊓ Filter.principal X) (nhds L)
All goals completed! 🐙
Твердження 9.9.15 / Вправа 9.9.5
theorem 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! 🐙
Теорема 9.9.16
theorem UniformContinuousOn.of_continuousOn {a b:ℝ} (hab: a < b) {f:ℝ → ℝ}
(hcont: ContinuousOn f (Set.Icc a b)) :
UniformContinuousOn f (Set.Icc a b) := a:ℝb:ℝhab:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)⊢ UniformContinuousOn f (Set.Icc a b)
-- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
a:ℝb:ℝhab:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)h:¬UniformContinuousOn f (Set.Icc a b)⊢ False
a:ℝb:ℝhab:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)h:¬∀ (x y : ℕ → ℝ),
(∀ (n : ℕ), x n ∈ Set.Icc a b) →
(∀ (n : ℕ), y n ∈ Set.Icc a b) →
{ m := 0, seq := fun n => if n ≥ 0 then x n.toNat else 0, vanish := ⋯ }.equiv
{ m := 0, seq := fun n => if n ≥ 0 then y n.toNat else 0, vanish := ⋯ } →
{ m := 0, seq := fun n => if n ≥ 0 then (f ∘ x) n.toNat else 0, vanish := ⋯ }.equiv
{ m := 0, seq := fun n => if n ≥ 0 then (f ∘ y) n.toNat else 0, vanish := ⋯ }⊢ False
a:ℝb:ℝhab:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)h:∃ x x_1,
∃ (_ : ∀ (n : ℕ), x n ∈ Set.Icc a b) (_ : ∀ (n : ℕ), x_1 n ∈ Set.Icc a b) (_ :
{ m := 0, seq := fun n => if 0 ≤ n then x n.toNat else 0, vanish := ⋯ }.equiv
{ m := 0, seq := fun n => if 0 ≤ n then x_1 n.toNat else 0, vanish := ⋯ }),
∃ 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:ℝhab:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)x:ℕ → ℝy:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a bhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:{ m := 0, seq := fun n => if 0 ≤ n then x n.toNat else 0, vanish := ⋯ }.equiv
{ m := 0, seq := fun n => if 0 ≤ n then y n.toNat else 0, vanish := ⋯ }ε:ℝ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:ℝhab:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)x:ℕ → ℝy:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a bhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:{ m := 0, seq := fun n => if 0 ≤ n then x n.toNat else 0, vanish := ⋯ }.equiv
{ m := 0, seq := fun n => if 0 ≤ n then y n.toNat else 0, vanish := ⋯ }ε:ℝ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 := a:ℝb:ℝhab:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)⊢ UniformContinuousOn f (Set.Icc a b)
a:ℝb:ℝhab:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)x:ℕ → ℝy:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a bhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:{ m := 0, seq := fun n => if 0 ≤ n then x n.toNat else 0, vanish := ⋯ }.equiv
{ m := 0, seq := fun n => if 0 ≤ n then y n.toNat else 0, vanish := ⋯ }ε:ℝ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
a:ℝb:ℝhab:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)x:ℕ → ℝy:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a bhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:{ m := 0, seq := fun n => if 0 ≤ n then x n.toNat else 0, vanish := ⋯ }.equiv
{ m := 0, seq := fun n => if 0 ≤ n then y n.toNat else 0, vanish := ⋯ }ε:ℝ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 : ε.eventually_close_seqs (fun n ↦ f (x n):Sequence) (fun n ↦ f (y n):Sequence) := a:ℝb:ℝhab:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)⊢ UniformContinuousOn f (Set.Icc a b)
All goals completed! 🐙
All goals completed! 🐙
have : Countable E := a:ℝb:ℝhab:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)⊢ UniformContinuousOn f (Set.Icc a b) All goals completed! 🐙
a:ℝb:ℝhab:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)x:ℕ → ℝy:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a bhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:{ m := 0, seq := fun n => if 0 ≤ n then x n.toNat else 0, vanish := ⋯ }.equiv
{ m := 0, seq := fun n => if 0 ≤ n then y n.toNat else 0, vanish := ⋯ }ε:ℝ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
a:ℝb:ℝhab:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)x:ℕ → ℝy:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a bhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:{ m := 0, seq := fun n => if 0 ≤ n then x n.toNat else 0, vanish := ⋯ }.equiv
{ m := 0, seq := fun n => if 0 ≤ n then y n.toNat else 0, vanish := ⋯ }ε:ℝ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 := a:ℝb:ℝhab:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)⊢ UniformContinuousOn f (Set.Icc a b)
a:ℝb:ℝhab:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)x:ℕ → ℝy:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a bhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:{ m := 0, seq := fun n => if 0 ≤ n then x n.toNat else 0, vanish := ⋯ }.equiv
{ m := 0, seq := fun n => if 0 ≤ n then y n.toNat else 0, vanish := ⋯ }ε:ℝ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⊢ (setOf E).Infinite
All goals completed! 🐙
a:ℝb:ℝhab:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)x:ℕ → ℝy:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a bhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:{ m := 0, seq := fun n => if 0 ≤ n then x n.toNat else 0, vanish := ⋯ }.equiv
{ m := 0, seq := fun n => if 0 ≤ n then y n.toNat else 0, vanish := ⋯ }ε:ℝ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))| > ε := a:ℝb:ℝhab:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)⊢ UniformContinuousOn f (Set.Icc a b)
a:ℝb:ℝhab:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)x:ℕ → ℝy:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a bhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:{ m := 0, seq := fun n => if 0 ≤ n then x n.toNat else 0, vanish := ⋯ }.equiv
{ m := 0, seq := fun n => if 0 ≤ n then y n.toNat else 0, vanish := ⋯ }ε:ℝ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))| > ε
a:ℝb:ℝhab:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)x:ℕ → ℝy:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a bhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:{ m := 0, seq := fun n => if 0 ≤ n then x n.toNat else 0, vanish := ⋯ }.equiv
{ m := 0, seq := fun n => if 0 ≤ n then y n.toNat else 0, vanish := ⋯ }ε:ℝ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:ε < |f (x (n j)) - f (y (n j))|⊢ |f (x (n j)) - f (y (n j))| > ε
All goals completed! 🐙
a:ℝb:ℝhab:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)x:ℕ → ℝy:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a bhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:{ m := 0, seq := fun n => if 0 ≤ n then x n.toNat else 0, vanish := ⋯ }.equiv
{ m := 0, seq := fun n => if 0 ≤ n then y n.toNat else 0, vanish := ⋯ }ε:ℝ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
a:ℝb:ℝhab:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)x:ℕ → ℝy:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a bhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:{ m := 0, seq := fun n => if 0 ≤ n then x n.toNat else 0, vanish := ⋯ }.equiv
{ m := 0, seq := fun n => if 0 ≤ n then y n.toNat else 0, vanish := ⋯ }ε:ℝ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
have hclosed : IsClosed (Set.Icc a b) := Icc_closed (a:ℝb:ℝhab:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)x:ℕ → ℝy:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a bhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:{ m := 0, seq := fun n => if 0 ≤ n then x n.toNat else 0, vanish := ⋯ }.equiv
{ m := 0, seq := fun n => if 0 ≤ n then y n.toNat else 0, vanish := ⋯ }ε:ℝ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⊢ a ≤ b All goals completed! 🐙)
a:ℝb:ℝhab:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)x:ℕ → ℝy:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a bhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:{ m := 0, seq := fun n => if 0 ≤ n then x n.toNat else 0, vanish := ⋯ }.equiv
{ m := 0, seq := fun n => if 0 ≤ n then y n.toNat else 0, vanish := ⋯ }ε:ℝ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
a:ℝb:ℝhab:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)x:ℕ → ℝy:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a bhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:{ m := 0, seq := fun n => if 0 ≤ n then x n.toNat else 0, vanish := ⋯ }.equiv
{ m := 0, seq := fun n => if 0 ≤ n then y n.toNat else 0, vanish := ⋯ }ε:ℝ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:Filter.Tendsto (fun j_1 => x (n (j j_1))) Filter.atTop (nhds L)⊢ False
a:ℝb:ℝhab:a < bf:ℝ → ℝx:ℕ → ℝy:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a bhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:{ m := 0, seq := fun n => if 0 ≤ n then x n.toNat else 0, vanish := ⋯ }.equiv
{ m := 0, seq := fun n => if 0 ≤ n then y n.toNat else 0, vanish := ⋯ }ε:ℝ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:Filter.Tendsto (fun j_1 => x (n (j j_1))) Filter.atTop (nhds L)hcont:ContinuousWithinAt f (Set.Icc a b) L⊢ False
a:ℝb:ℝhab:a < bf:ℝ → ℝx:ℕ → ℝy:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a bhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:{ m := 0, seq := fun n => if 0 ≤ n then x n.toNat else 0, vanish := ⋯ }.equiv
{ m := 0, seq := fun n => if 0 ≤ n then y n.toNat else 0, vanish := ⋯ }ε:ℝ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:Filter.Tendsto (fun j_1 => x (n (j j_1))) Filter.atTop (nhds L)hcont:ContinuousWithinAt f (Set.Icc a b) Lhconv':Filter.Tendsto (fun n_1 => f (x (n (j n_1)))) Filter.atTop (nhds (f L))⊢ False
a:ℝb:ℝhab:a < bf:ℝ → ℝx:ℕ → ℝy:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a bhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:Filter.Tendsto
(fun n =>
{ m := 0, seq := fun n => if 0 ≤ n then x n.toNat else 0, vanish := ⋯ }.seq n -
{ m := 0, seq := fun n => if 0 ≤ n then y n.toNat else 0, vanish := ⋯ }.seq n)
Filter.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:Filter.Tendsto (fun j_1 => x (n (j j_1))) Filter.atTop (nhds L)hcont:ContinuousWithinAt f (Set.Icc a b) Lhconv':Filter.Tendsto (fun n_1 => f (x (n (j n_1)))) Filter.atTop (nhds (f L))⊢ False
replace hequiv : Filter.Tendsto (fun k ↦ x (n (j k)) - y (n (j k))) Filter.atTop (nhds 0) := a:ℝb:ℝhab:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)⊢ UniformContinuousOn f (Set.Icc a b)
a:ℝb:ℝhab:a < bf:ℝ → ℝx:ℕ → ℝy:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a bhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:Filter.Tendsto
(fun n =>
{ m := 0, seq := fun n => if 0 ≤ n then x n.toNat else 0, vanish := ⋯ }.seq n -
{ m := 0, seq := fun n => if 0 ≤ n then y n.toNat else 0, vanish := ⋯ }.seq n)
Filter.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:Filter.Tendsto (fun j_1 => x (n (j j_1))) Filter.atTop (nhds L)hcont:ContinuousWithinAt f (Set.Icc a b) Lhconv':Filter.Tendsto (fun n_1 => f (x (n (j n_1)))) Filter.atTop (nhds (f L))hj':Filter.Tendsto j Filter.atTop Filter.atTop⊢ Filter.Tendsto (fun k => x (n (j k)) - y (n (j k))) Filter.atTop (nhds 0)
a:ℝb:ℝhab:a < bf:ℝ → ℝx:ℕ → ℝy:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a bhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:Filter.Tendsto
(fun n =>
{ m := 0, seq := fun n => if 0 ≤ n then x n.toNat else 0, vanish := ⋯ }.seq n -
{ m := 0, seq := fun n => if 0 ≤ n then y n.toNat else 0, vanish := ⋯ }.seq n)
Filter.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:Filter.Tendsto (fun j_1 => x (n (j j_1))) Filter.atTop (nhds L)hcont:ContinuousWithinAt f (Set.Icc a b) Lhconv':Filter.Tendsto (fun n_1 => f (x (n (j n_1)))) Filter.atTop (nhds (f L))hj':Filter.Tendsto j Filter.atTop Filter.atTophn':Filter.Tendsto n Filter.atTop Filter.atTop⊢ Filter.Tendsto (fun k => x (n (j k)) - y (n (j k))) Filter.atTop (nhds 0)
a:ℝb:ℝhab:a < bf:ℝ → ℝx:ℕ → ℝy:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a bhy:∀ (n : ℕ), y n ∈ Set.Icc a bhequiv:Filter.Tendsto
(fun n =>
{ m := 0, seq := fun n => if 0 ≤ n then x n.toNat else 0, vanish := ⋯ }.seq n -
{ m := 0, seq := fun n => if 0 ≤ n then y n.toNat else 0, vanish := ⋯ }.seq n)
Filter.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:Filter.Tendsto (fun j_1 => x (n (j j_1))) Filter.atTop (nhds L)hcont:ContinuousWithinAt f (Set.Icc a b) Lhconv':Filter.Tendsto (fun n_1 => f (x (n (j n_1)))) Filter.atTop (nhds (f L))hj':Filter.Tendsto j Filter.atTop Filter.atTophn':Filter.Tendsto n Filter.atTop Filter.atTophcoe:Filter.Tendsto (fun n => ↑n) Filter.atTop Filter.atTop⊢ Filter.Tendsto (fun k => x (n (j k)) - y (n (j k))) Filter.atTop (nhds 0)
All goals completed! 🐙
have hyconv : Filter.Tendsto (fun k ↦ y (n (j k))) Filter.atTop (nhds L) := a:ℝb:ℝhab:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)⊢ UniformContinuousOn f (Set.Icc a b)
a:ℝb:ℝhab:a < bf:ℝ → ℝx:ℕ → ℝy:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a bhy:∀ (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:Filter.Tendsto (fun j_1 => x (n (j j_1))) Filter.atTop (nhds L)hcont:ContinuousWithinAt f (Set.Icc a b) Lhconv':Filter.Tendsto (fun n_1 => f (x (n (j n_1)))) Filter.atTop (nhds (f L))hequiv:Filter.Tendsto (fun k => x (n (j k)) - y (n (j k))) Filter.atTop (nhds 0)k:ℕ⊢ y (n (j k)) = x (n (j k)) - (x (n (j k)) - y (n (j k)))a:ℝb:ℝhab:a < bf:ℝ → ℝx:ℕ → ℝy:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a bhy:∀ (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:Filter.Tendsto (fun j_1 => x (n (j j_1))) Filter.atTop (nhds L)hcont:ContinuousWithinAt f (Set.Icc a b) Lhconv':Filter.Tendsto (fun n_1 => f (x (n (j n_1)))) Filter.atTop (nhds (f L))hequiv:Filter.Tendsto (fun k => x (n (j k)) - y (n (j k))) Filter.atTop (nhds 0)⊢ L = L - 0
a:ℝb:ℝhab:a < bf:ℝ → ℝx:ℕ → ℝy:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a bhy:∀ (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:Filter.Tendsto (fun j_1 => x (n (j j_1))) Filter.atTop (nhds L)hcont:ContinuousWithinAt f (Set.Icc a b) Lhconv':Filter.Tendsto (fun n_1 => f (x (n (j n_1)))) Filter.atTop (nhds (f L))hequiv:Filter.Tendsto (fun k => x (n (j k)) - y (n (j k))) Filter.atTop (nhds 0)k:ℕ⊢ y (n (j k)) = x (n (j k)) - (x (n (j k)) - y (n (j k))) All goals completed! 🐙
All goals completed! 🐙
a:ℝb:ℝhab:a < bf:ℝ → ℝx:ℕ → ℝy:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a bhy:∀ (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:Filter.Tendsto (fun j_1 => x (n (j j_1))) Filter.atTop (nhds L)hcont:ContinuousWithinAt f (Set.Icc a b) Lhconv':Filter.Tendsto (fun n_1 => f (x (n (j n_1)))) Filter.atTop (nhds (f L))hequiv:Filter.Tendsto (fun k => x (n (j k)) - y (n (j k))) Filter.atTop (nhds 0)hyconv:Filter.Tendsto (fun n_1 => f (y (n (j n_1)))) Filter.atTop (nhds (f L))⊢ False
have : Filter.Tendsto (fun k ↦ f (x (n (j k))) - f (y (n (j k)))) Filter.atTop (nhds 0) := a:ℝb:ℝhab:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)⊢ UniformContinuousOn f (Set.Icc a b)
a:ℝb:ℝhab:a < bf:ℝ → ℝx:ℕ → ℝy:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Icc a bhy:∀ (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:Filter.Tendsto (fun j_1 => x (n (j j_1))) Filter.atTop (nhds L)hcont:ContinuousWithinAt f (Set.Icc a b) Lhconv':Filter.Tendsto (fun n_1 => f (x (n (j n_1)))) Filter.atTop (nhds (f L))hequiv:Filter.Tendsto (fun k => x (n (j k)) - y (n (j k))) Filter.atTop (nhds 0)hyconv:Filter.Tendsto (fun n_1 => f (y (n (j n_1)))) Filter.atTop (nhds (f L))⊢ 0 = f L - f L
All goals completed! 🐙
All goals completed! 🐙
Вправа 9.9.6
theorem 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