Аналіз 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:

open Chapter6namespace Chapter9declaration uses 'sorry'example : ContinuousOn (fun x: 1/x) (Set.Icc 0 2) := ContinuousOn (fun x => 1 / x) (Set.Icc 0 2) All goals completed! 🐙declaration uses 'sorry'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

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₀| ε 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₀| ε 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₀| ε 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₀| ε All goals completed! 🐙

Визначення 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₀) ε 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 ε::ε > 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 ε::ε > 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 ε::ε > 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 ε::ε > 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 ε::ε > 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 ε::ε > 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 ε::ε > 0δ::δ > 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 ε::ε > 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₀) ε All goals completed! 🐙 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 XContinuousOn 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

Визначення 9.9.5. This is similar but not identical to Real.close_seq (ε : ℝ) (a : Sequence) (L : ℝ) : PropReal.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 declaration uses 'sorry'Chapter6.Sequence.equiv_iff_rat (a b: Sequence) : Sequence.equiv a b ε > (0:), (ε:).eventually_close_seqs a b := a:Sequenceb:Sequencea.equiv b ε > 0, (↑ε).eventually_close_seqs a b All goals completed! 🐙

Лема 9.9.7 / Вправа 9.9.1

theorem declaration uses 'sorry'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:Sequencea.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 declaration uses 'sorry'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 declaration uses 'sorry'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! 🐙

Приклад 9.9.10

noncomputable abbrev f_9_9_10 : := fun x 1/x
declaration uses 'sorry'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! 🐙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 : ¬ 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! 🐙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! 🐙

Приклад 9.9.11

abbrev f_9_9_11 : := fun x x^2
declaration uses 'sorry'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! 🐙declaration uses 'sorry'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! 🐙declaration uses 'sorry'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 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:{ 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

declaration uses 'sorry'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! 🐙
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 := ¬{ 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! 🐙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! 🐙

Наслідок 9.9.14 / Вправа 9.9.4

theorem declaration uses 'sorry'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 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 EBornology.IsBounded (f '' E) All goals completed! 🐙

Теорема 9.9.16

theorem declaration uses 'sorry'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 := }ε::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 := }ε::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 := }ε::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 := }ε::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 EFalse 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 := }ε::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 EFalse 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 := }ε::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 EFalse 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 := }ε::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 := }ε::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 EFalse 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 := }ε::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 := }ε::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 := }ε::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 bFalse 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 := }ε::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 bFalse 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 := }ε::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 ba 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 := }ε::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 := }ε::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 := }ε::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) LFalse 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 := }ε::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)ε::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)ε::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.atTopFilter.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)ε::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.atTopFilter.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)ε::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.atTopFilter.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ε::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ε::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ε::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ε::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ε::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 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 YUniformContinuousOn (g f) X All goals completed! 🐙
end Chapter9