Аналіз I, Глава 5.5

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.

In this section we begin to use the Mathlib API for sets; the Chapter 3 set theory is deprecated in favor of this API.

Main constructions and results of this section:

namespace Chapter5

Визначення 5.5.1 (upper bounds). Here we use the upperBounds.{u_1} {α : Type u_1} [LE α] (s : Set α) : Set αupperBounds set defined in Mathlib.

theorem Real.upperBound_def (E: Set Real) (M: Real) : M ∈ upperBounds E ↔ ∀ x ∈ E, x ≤ M := mem_upperBounds
theorem Real.lowerBound_def (E: Set Real) (M: Real) : M ∈ lowerBounds E ↔ ∀ x ∈ E, x ≥ M := mem_lowerBounds

API for Example 5.5.2

theorem Real.Icc_def (x y:Real) : Set.Icc x y = { z | x ≤ z ∧ z ≤ y } := rfl

API for Example 5.5.2

theorem Real.mem_Icc (x y z:Real) : z ∈ Set.Icc x y ↔ x ≤ z ∧ z ≤ y := x:Realy:Realz:Real⊢ z ∈ Set.Icc x y ↔ x ≤ z ∧ z ≤ y All goals completed! 🐙

Приклад 5.5.2

declaration uses 'sorry'example (M: Real) : M ∈ upperBounds (Set.Icc 0 1) ↔ M ≥ 1 := M:Real⊢ M ∈ upperBounds (Set.Icc 0 1) ↔ M ≥ 1 All goals completed! 🐙

API for Example 5.5.3

theorem Real.Ioi_def (x:Real) : Set.Ioi x = { z | z > x } := rfl

Приклад 5.5.3

declaration uses 'sorry'example : ¬ ∃ M, M ∈ upperBounds (Set.Ioi 0) := ⊢ ¬∃ M, M ∈ upperBounds (Set.Ioi 0) All goals completed! 🐙

Приклад 5.5.4

declaration uses 'sorry'example : ∀ M, M ∈ upperBounds (∅ : Set Real) := ⊢ ∀ (M : Real), M ∈ upperBounds ∅ All goals completed! 🐙
theorem declaration uses 'sorry'Real.upperBound_upper {M M': Real} (h: M ≤ M') {E: Set Real} (hb: M ∈ upperBounds E) : M' ∈ upperBounds E := M:RealM':Realh:M ≤ M'E:Set Realhb:M ∈ upperBounds E⊢ M' ∈ upperBounds E All goals completed! 🐙

Визначення 5.5.5 (least upper bound). Here we use the unknown identifier 'isLUB'isLUB predicate defined in Mathlib.

theorem Real.isLUB_def (E: Set Real) (M: Real) : IsLUB E M ↔ M ∈ upperBounds E ∧ ∀ M' ∈ upperBounds E, M' ≥ M := E:Set RealM:Real⊢ IsLUB E M ↔ M ∈ upperBounds E ∧ ∀ M' ∈ upperBounds E, M' ≥ M E:Set RealM:Real⊢ IsLUB E M ↔ M ∈ upperBounds E ∧ ∀ M' ∈ upperBounds E, M ≤ M' All goals completed! 🐙
theorem Real.isGLB_def (E: Set Real) (M: Real) : IsGLB E M ↔ M ∈ lowerBounds E ∧ ∀ M' ∈ lowerBounds E, M' ≤ M := E:Set RealM:Real⊢ IsGLB E M ↔ M ∈ lowerBounds E ∧ ∀ M' ∈ lowerBounds E, M' ≤ M All goals completed! 🐙

Приклад 5.5.6

declaration uses 'sorry'example : IsLUB (Set.Icc 0 1) 1 := ⊢ IsLUB (Set.Icc 0 1) 1 All goals completed! 🐙

Приклад 5.5.7

declaration uses 'sorry'example : ¬∃ M, IsLUB (∅: Set Real) M := ⊢ ¬∃ M, IsLUB ∅ M All goals completed! 🐙

Твердження 5.5.8 (Uniqueness of least upper bound)

theorem Real.LUB_unique {E: Set Real} {M M': Real} (h1: IsLUB E M) (h2: IsLUB E M') : M = M' := E:Set RealM:RealM':Realh1:IsLUB E Mh2:IsLUB E M'⊢ M = M' -- цей доказ написан так, щоб співпадати із структурою орігінального тексту. E:Set RealM:RealM':Realh1:M ∈ upperBounds E ∧ ∀ M' ∈ upperBounds E, M' ≥ Mh2:M' ∈ upperBounds E ∧ ∀ M'_1 ∈ upperBounds E, M'_1 ≥ M'⊢ M = M' E:Set RealM:RealM':Realh1:M ∈ upperBounds E ∧ ∀ M' ∈ upperBounds E, M' ≥ Mh2:M' ∈ upperBounds E ∧ ∀ M'_1 ∈ upperBounds E, M'_1 ≥ M'h3:M' ≥ M⊢ M = M' E:Set RealM:RealM':Realh1:M ∈ upperBounds E ∧ ∀ M' ∈ upperBounds E, M' ≥ Mh2:M' ∈ upperBounds E ∧ ∀ M'_1 ∈ upperBounds E, M'_1 ≥ M'h3:M' ≥ Mh4:M ≥ M'⊢ M = M' All goals completed! 🐙

Визначення of "bounded above", using Mathlib notation

theorem Real.bddAbove_def (E: Set Real) : BddAbove E ↔ ∃ M, M ∈ upperBounds E := Set.nonempty_def
theorem Real.bddBelow_def (E: Set Real) : BddBelow E ↔ ∃ M, M ∈ lowerBounds E := Set.nonempty_def

Вправа 5.5.2

theorem declaration uses 'sorry'Real.upperBound_between {E: Set Real} {n:ℕ} {L K:ℤ} (hLK: L < K) (hK: K*((1/(n+1):ℚ):Real) ∈ upperBounds E) (hL: L*((1/(n+1):ℚ):Real) ∉ upperBounds E) : ∃ m, L < m ∧ m ≤ K ∧ m*((1/(n+1):ℚ):Real) ∈ upperBounds E ∧ (m-1)*((1/(n+1):ℚ):Real) ∉ upperBounds E := E:Set Realn:ℕL:ℤK:ℤhLK:L < KhK:↑K * ↑(1 / (↑n + 1)) ∈ upperBounds EhL:↑L * ↑(1 / (↑n + 1)) ∉ upperBounds E⊢ ∃ m, L < m ∧ m ≤ K ∧ ↑m * ↑(1 / (↑n + 1)) ∈ upperBounds E ∧ (↑m - 1) * ↑(1 / (↑n + 1)) ∉ upperBounds E All goals completed! 🐙

Вправа 5.5.3

theorem declaration uses 'sorry'Real.upperBound_discrete_unique {E: Set Real} {n:ℕ} {m m':ℤ} (hm1: (((m:ℚ) / (n+1):ℚ):Real) ∈ upperBounds E) (hm2: (((m:ℚ) / (n+1) - 1 / (n+1):ℚ):Real) ∉ upperBounds E) (hm'1: (((m':ℚ) / (n+1):ℚ):Real) ∈ upperBounds E) (hm'2: (((m':ℚ) / (n+1) - 1 / (n+1):ℚ):Real) ∉ upperBounds E) : m = m' := E:Set Realn:ℕm:ℤm':ℤhm1:↑(↑m / (↑n + 1)) ∈ upperBounds Ehm2:↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Ehm'1:↑(↑m' / (↑n + 1)) ∈ upperBounds Ehm'2:↑(↑m' / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E⊢ m = m' All goals completed! 🐙

Вправа 5.5.4

theorem declaration uses 'sorry'Real.LIM_of_Cauchy {q:ℕ → ℚ} (hq: ∀ M, ∀ n ≥ M, ∀ n' ≥ M, |q n - q n'| ≤ 1 / (M+1)) : (q:Sequence).isCauchy ∧ ∀ M, |q M - LIM q| ≤ 1 / (M+1) := q:ℕ → ℚhq:∀ (M n : ℕ), n ≥ M → ∀ n' ≥ M, |q n - q n'| ≤ 1 / (↑M + 1)⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then q n.toNat else 0, vanish := ⋯ }.isCauchy ∧ ∀ (M : ℕ), |↑(q M) - LIM q| ≤ 1 / (↑M + 1) All goals completed! 🐙

Теорема 5.5.9 (Existence of least upper bound)

theorem Real.LUB_exist {E: Set Real} (hE: Set.Nonempty E) (hbound: BddAbove E): ∃ S, IsLUB E S := E:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃ S, IsLUB E S -- цей доказ написан так, щоб співпадати із структурою орігінального тексту. E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.some⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ E⊢ ∃ S, IsLUB E S have claim1 (n:ℕ) : ∃! m:ℤ, (((m:ℚ) / (n+1):ℚ):Real) ∈ upperBounds E ∧ ¬ (((m:ℚ) / (n+1) - 1 / (n+1):ℚ):Real) ∈ upperBounds E := E:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))⊢ ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E have hpos : ε.isPos := E:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))⊢ 0 < ↑n + 1 All goals completed! 🐙 E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPos⊢ ∃ x, ↑(↑x / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑x / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds EE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPos⊢ ∀ (y₁ y₂ : ℤ), ↑(↑y₁ / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑y₁ / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E → ↑(↑y₂ / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑y₂ / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E → y₁ = y₂ E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPos⊢ ∃ x, ↑(↑x / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑x / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E E:Set RealhE:E.Nonemptyhbound:∃ M, M ∈ upperBounds Ex₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPos⊢ ∃ x, ↑(↑x / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑x / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E E:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPosM:Realhbound:M ∈ upperBounds E⊢ ∃ x, ↑(↑x / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑x / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E E:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPosM:Realhbound:M ∈ upperBounds EK:ℕleft✝:K > 0hK:↑K * ε > M⊢ ∃ x, ↑(↑x / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑x / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E E:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPosM:Realhbound:M ∈ upperBounds EK:ℕleft✝¹:K > 0hK:↑K * ε > ML':ℕleft✝:L' > 0hL:↑L' * ε > -x₀⊢ ∃ x, ↑(↑x / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑x / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E E:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPosM:Realhbound:M ∈ upperBounds EK:ℕleft✝¹:K > 0hK:↑K * ε > ML':ℕleft✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'⊢ ∃ x, ↑(↑x / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑x / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E have claim1_1 : L * ε < x₀ := E:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPosM:Realhbound:M ∈ upperBounds EK:ℕleft✝¹:K > 0hK:↑K * ε > ML':ℕleft✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'⊢ -(↑L' * ε) < x₀; All goals completed! 🐙 have claim1_2 : L * ε ∉ upperBounds E := E:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPosM:Realhbound:M ∈ upperBounds EK:ℕleft✝¹:K > 0hK:↑K * ε > ML':ℕleft✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε ∈ upperBounds E⊢ x₀ ≤ ↑L * ε E:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPosM:Realhbound:M ∈ upperBounds EK:ℕleft✝¹:K > 0hK:↑K * ε > ML':ℕleft✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:∀ x ∈ E, x ≤ ↑L * ε⊢ x₀ ≤ ↑L * ε All goals completed! 🐙 have claim1_3 : (K:Real) > (L:Real) := E:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPosM:Realhbound:M ∈ upperBounds EK:ℕleft✝¹:K > 0hK:↑K * ε > ML':ℕleft✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:↑K ≤ ↑L⊢ ↑L * ε ∈ upperBounds E E:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPosM:Realhbound:M ∈ upperBounds EK:ℕleft✝¹:K > 0hK:↑K * ε > ML':ℕleft✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:ε * ↑K ≤ ε * ↑L⊢ ↑L * ε ∈ upperBounds E E:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPosM:Realhbound:M ∈ upperBounds EK:ℕleft✝¹:K > 0hK:↑K * ε > ML':ℕleft✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:↑K * ε ≤ ↑L * ε⊢ ↑L * ε ∈ upperBounds E E:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPosM:Realhbound:M ∈ upperBounds EK:ℕleft✝¹:K > 0hK:↑K * ε > ML':ℕleft✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:M < ↑L * ε⊢ ↑L * ε ∈ upperBounds E All goals completed! 🐙 have claim1_4 : ∃ m:ℤ, L < m ∧ m ≤ K ∧ m*ε ∈ upperBounds E ∧ (m-1)*ε ∉ upperBounds E := E:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPosM:Realhbound:M ∈ upperBounds EK:ℕleft✝¹:K > 0hK:↑K * ε > ML':ℕleft✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:↑L * ε ∉ upperBounds Eclaim1_3:↑K > ↑L⊢ L < ↑KE:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPosM:Realhbound:M ∈ upperBounds EK:ℕleft✝¹:K > 0hK:↑K * ε > ML':ℕleft✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:↑L * ε ∉ upperBounds Eclaim1_3:↑K > ↑L⊢ ↑↑K * ↑(1 / (↑n + 1)) ∈ upperBounds E E:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPosM:Realhbound:M ∈ upperBounds EK:ℕleft✝¹:K > 0hK:↑K * ε > ML':ℕleft✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:↑L * ε ∉ upperBounds Eclaim1_3:↑K > ↑L⊢ L < ↑K E:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPosM:Realhbound:M ∈ upperBounds EK:ℕleft✝¹:K > 0hK:↑K * ε > ML':ℕleft✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:↑L * ε ∉ upperBounds Eclaim1_3:↑K > ↑L⊢ ↑L < ↑K E:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPosM:Realhbound:M ∈ upperBounds EK:ℕleft✝¹:K > 0hK:↑K * ε > ML':ℕleft✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:↑L * ε ∉ upperBounds Eclaim1_3:↑K > ↑L⊢ ↑↑K > ↑↑L All goals completed! 🐙 E:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPosM:Realhbound:M ∈ upperBounds EK:ℕleft✝¹:K > 0hK:↑K * ε > ML':ℕleft✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:↑L * ε ∉ upperBounds Eclaim1_3:↑K > ↑L⊢ M < ↑↑K * ↑(1 / (↑n + 1)) E:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPosM:Realhbound:M ∈ upperBounds EK:ℕleft✝¹:K > 0hK:↑K * ε > ML':ℕleft✝:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:↑L * ε ∉ upperBounds Eclaim1_3:↑K > ↑L⊢ ↑↑K * ↑(1 / (↑n + 1)) > M All goals completed! 🐙 E:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPosM:Realhbound:M ∈ upperBounds EK:ℕleft✝³:K > 0hK:↑K * ε > ML':ℕleft✝²:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:↑L * ε ∉ upperBounds Eclaim1_3:↑K > ↑Lm:ℤleft✝¹:L < mleft✝:m ≤ ↑Khm:↑m * ε ∈ upperBounds Ehm':(↑m - 1) * ε ∉ upperBounds E⊢ ∃ x, ↑(↑x / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑x / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E E:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPosM:Realhbound:M ∈ upperBounds EK:ℕleft✝³:K > 0hK:↑K * ε > ML':ℕleft✝²:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:↑L * ε ∉ upperBounds Eclaim1_3:↑K > ↑Lm:ℤleft✝¹:L < mleft✝:m ≤ ↑Khm:↑m * ε ∈ upperBounds Ehm':(↑m - 1) * ε ∉ upperBounds E⊢ ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E have : (m/(n+1):ℚ) = m*ε := E:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPosM:Realhbound:M ∈ upperBounds EK:ℕleft✝³:K > 0hK:↑K * ε > ML':ℕleft✝²:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:↑L * ε ∉ upperBounds Eclaim1_3:↑K > ↑Lm:ℤleft✝¹:L < mleft✝:m ≤ ↑Khm:↑m * ε ∈ upperBounds Ehm':(↑m - 1) * ε ∉ upperBounds E⊢ ↑m / (↑n + 1) = ↑m * (↑n + 1)⁻¹ All goals completed! 🐙 E:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPosM:Realhbound:M ∈ upperBounds EK:ℕleft✝³:K > 0hK:↑K * ε > ML':ℕleft✝²:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:↑L * ε ∉ upperBounds Eclaim1_3:↑K > ↑Lm:ℤleft✝¹:L < mleft✝:m ≤ ↑Khm:↑m * ε ∈ upperBounds Ehm':(↑m - 1) * ε ∉ upperBounds Ethis:↑(↑m / (↑n + 1)) = ↑m * ε⊢ ↑(↑m / (↑n + 1)) ∈ upperBounds EE:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPosM:Realhbound:M ∈ upperBounds EK:ℕleft✝³:K > 0hK:↑K * ε > ML':ℕleft✝²:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:↑L * ε ∉ upperBounds Eclaim1_3:↑K > ↑Lm:ℤleft✝¹:L < mleft✝:m ≤ ↑Khm:↑m * ε ∈ upperBounds Ehm':(↑m - 1) * ε ∉ upperBounds Ethis:↑(↑m / (↑n + 1)) = ↑m * ε⊢ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E E:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPosM:Realhbound:M ∈ upperBounds EK:ℕleft✝³:K > 0hK:↑K * ε > ML':ℕleft✝²:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:↑L * ε ∉ upperBounds Eclaim1_3:↑K > ↑Lm:ℤleft✝¹:L < mleft✝:m ≤ ↑Khm:↑m * ε ∈ upperBounds Ehm':(↑m - 1) * ε ∉ upperBounds Ethis:↑(↑m / (↑n + 1)) = ↑m * ε⊢ ↑(↑m / (↑n + 1)) ∈ upperBounds E All goals completed! 🐙 E:Set RealhE:E.Nonemptyx₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPosM:Realhbound:M ∈ upperBounds EK:ℕleft✝³:K > 0hK:↑K * ε > ML':ℕleft✝²:L' > 0hL:↑L' * ε > -x₀L:ℤ := -↑L'claim1_1:↑L * ε < x₀claim1_2:↑L * ε ∉ upperBounds Eclaim1_3:↑K > ↑Lm:ℤleft✝¹:L < mleft✝:m ≤ ↑Khm:↑m * ε ∈ upperBounds Ehm':(↑m - 1) * ε ∉ upperBounds Ethis:↑(↑m / (↑n + 1)) = ↑m * ε⊢ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) = (↑m - 1) * ε All goals completed! 🐙 -- Вправа 5.5.3 E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ En:ℕε:Real := ↑(1 / (↑n + 1))hpos:ε.isPosm:ℤm':ℤhm1:↑(↑m / (↑n + 1)) ∈ upperBounds Ehm2:↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Ehm'1:↑(↑m' / (↑n + 1)) ∈ upperBounds Ehm'2:↑(↑m' / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E⊢ m = m' All goals completed! 🐙 E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choose⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchy⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds E⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds E⊢ ∃ S, IsLUB E S have claim2 (N:ℕ) : ∀ n ≥ N, ∀ n' ≥ N, |a n - a n'| ≤ 1 / (N+1) := E:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds EN:ℕn:ℕhn:n ≥ Nn':ℕhn':n' ≥ N⊢ |a n - a n'| ≤ 1 / (↑N + 1) E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds EN:ℕn:ℕhn:n ≥ Nn':ℕhn':n' ≥ N⊢ -(1 / (↑N + 1)) ≤ a n - a n' ∧ a n - a n' ≤ 1 / (↑N + 1) E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds EN:ℕn:ℕhn:n ≥ Nn':ℕhn':n' ≥ N⊢ -(1 / (↑N + 1)) ≤ a n - a n'E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds EN:ℕn:ℕhn:n ≥ Nn':ℕhn':n' ≥ N⊢ a n - a n' ≤ 1 / (↑N + 1) E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds EN:ℕn:ℕhn:n ≥ Nn':ℕhn':n' ≥ N⊢ -(1 / (↑N + 1)) ≤ a n - a n' E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds EN:ℕn:ℕhn:n ≥ Nn':ℕhn':n' ≥ Nhm1:↑(a n) ∈ upperBounds E⊢ -(1 / (↑N + 1)) ≤ a n - a n'; E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyN:ℕn:ℕhn:n ≥ Nn':ℕhn':n' ≥ Nhm1:↑(a n) ∈ upperBounds Ehm2:↑((a - b) n') ∉ upperBounds E⊢ -(1 / (↑N + 1)) ≤ a n - a n' have bound1 : ((a-b) n') < a n := E:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyN:ℕn:ℕhn:n ≥ Nn':ℕhn':n' ≥ Nhm1:↑(a n) ∈ upperBounds Ehm2:↑((a - b) n') ∉ upperBounds E⊢ ↑((a - b) n') < ↑(a n) E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyN:ℕn:ℕhn:n ≥ Nn':ℕhn':n' ≥ Nhm1:↑(a n) ∈ upperBounds Ehm2:↑(a n) ≤ ↑((a - b) n')⊢ ↑((a - b) n') ∈ upperBounds E All goals completed! 🐙 have bound2 : ((a-b) n') = a n' - 1 / (n'+1) := E:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃ S, IsLUB E S All goals completed! 🐙 have bound3 : 1/((n':ℚ)+1) ≤ 1/(N+1) := E:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃ S, IsLUB E S All goals completed! 🐙 All goals completed! 🐙 E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds EN:ℕn:ℕhn:n ≥ Nn':ℕhn':n' ≥ Nhm1:↑(a n') ∈ upperBounds E⊢ a n - a n' ≤ 1 / (↑N + 1); E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyN:ℕn:ℕhn:n ≥ Nn':ℕhn':n' ≥ Nhm1:↑(a n') ∈ upperBounds Ehm2:↑((a - b) n) ∉ upperBounds E⊢ a n - a n' ≤ 1 / (↑N + 1) have bound1 : ((a-b) n) < a n' := E:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyN:ℕn:ℕhn:n ≥ Nn':ℕhn':n' ≥ Nhm1:↑(a n') ∈ upperBounds Ehm2:↑((a - b) n) ∉ upperBounds E⊢ ↑((a - b) n) < ↑(a n') E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyN:ℕn:ℕhn:n ≥ Nn':ℕhn':n' ≥ Nhm1:↑(a n') ∈ upperBounds Ehm2:↑(a n') ≤ ↑((a - b) n)⊢ ↑((a - b) n) ∈ upperBounds E All goals completed! 🐙 have bound2 : ((a-b) n) = a n - 1 / (n+1) := E:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃ S, IsLUB E S All goals completed! 🐙 have bound3 : 1/((n+1):ℚ) ≤ 1/(N+1) := E:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃ S, IsLUB E S All goals completed! 🐙 -- weirdly, `linarith` times out here, so we proceed manually E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyN:ℕn:ℕhn:n ≥ Nn':ℕhn':n' ≥ Nhm1:↑(a n') ∈ upperBounds Ehm2:↑((a - b) n) ∉ upperBounds Ebound1:a n - 1 / (↑n + 1) < a n'bound2:(a - b) n = a n - 1 / (↑n + 1)bound3:1 / (↑n + 1) ≤ 1 / (↑N + 1)⊢ a n - a n' ≤ 1 / (↑N + 1) E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyN:ℕn:ℕhn:n ≥ Nn':ℕhn':n' ≥ Nhm1:↑(a n') ∈ upperBounds Ehm2:↑((a - b) n) ∉ upperBounds Ebound1:a n - 1 / (↑n + 1) < a n'bound2:(a - b) n = a n - 1 / (↑n + 1)bound3:1 / (↑n + 1) ≤ 1 / (↑N + 1)⊢ a n - a n' < 1 / (↑n + 1) rwa [sub_lt_commE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyN:ℕn:ℕhn:n ≥ Nn':ℕhn':n' ≥ Nhm1:↑(a n') ∈ upperBounds Ehm2:↑((a - b) n) ∉ upperBounds Ebound1:a n - 1 / (↑n + 1) < a n'bound2:(a - b) n = a n - 1 / (↑n + 1)bound3:1 / (↑n + 1) ≤ 1 / (↑N + 1)⊢ a n - 1 / (↑n + 1) < a n' E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |a n - a n'| ≤ 1 / (↑N + 1)claim3:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |a n - a n'| ≤ 1 / (↑N + 1)claim3:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyS:Real := LIM a⊢ ∃ S, IsLUB E S have claim4 : S = LIM (a - b) := E:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |a n - a n'| ≤ 1 / (↑N + 1)claim3:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyS:Real := LIM athis:LIM b = 0⊢ S = LIM (a - b) All goals completed! 🐙 E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |a n - a n'| ≤ 1 / (↑N + 1)claim3:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyS:Real := LIM aclaim4:S = LIM (a - b)⊢ IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |a n - a n'| ≤ 1 / (↑N + 1)claim3:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyS:Real := LIM aclaim4:S = LIM (a - b)⊢ (∀ x ∈ E, x ≤ S) ∧ ∀ M' ∈ upperBounds E, M' ≥ S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |a n - a n'| ≤ 1 / (↑N + 1)claim3:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyS:Real := LIM aclaim4:S = LIM (a - b)⊢ ∀ x ∈ E, x ≤ SE:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |a n - a n'| ≤ 1 / (↑N + 1)claim3:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyS:Real := LIM aclaim4:S = LIM (a - b)⊢ ∀ M' ∈ upperBounds E, M' ≥ S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |a n - a n'| ≤ 1 / (↑N + 1)claim3:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyS:Real := LIM aclaim4:S = LIM (a - b)⊢ ∀ x ∈ E, x ≤ S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |a n - a n'| ≤ 1 / (↑N + 1)claim3:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyS:Real := LIM aclaim4:S = LIM (a - b)x:Realhx:x ∈ E⊢ x ≤ S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |a n - a n'| ≤ 1 / (↑N + 1)claim3:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyS:Real := LIM aclaim4:S = LIM (a - b)x:Realhx:x ∈ E⊢ LIM a ≥ x E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |a n - a n'| ≤ 1 / (↑N + 1)claim3:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyS:Real := LIM aclaim4:S = LIM (a - b)x:Realhx:x ∈ E⊢ ∀ (n : ℕ), ↑(a n) ≥ x E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |a n - a n'| ≤ 1 / (↑N + 1)claim3:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyS:Real := LIM aclaim4:S = LIM (a - b)x:Realhx:x ∈ En:ℕ⊢ ↑(a n) ≥ x E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |a n - a n'| ≤ 1 / (↑N + 1)claim3:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyS:Real := LIM aclaim4:S = LIM (a - b)x:Realhx:x ∈ En:ℕhm1:↑(a n) ∈ upperBounds E⊢ ↑(a n) ≥ x E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |a n - a n'| ≤ 1 / (↑N + 1)claim3:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyS:Real := LIM aclaim4:S = LIM (a - b)x:Realhx:x ∈ En:ℕhm1:∀ x ∈ E, x ≤ ↑(a n)⊢ ↑(a n) ≥ x All goals completed! 🐙 E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |a n - a n'| ≤ 1 / (↑N + 1)claim3:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyS:Real := LIM aclaim4:S = LIM (a - b)y:Realhy:y ∈ upperBounds E⊢ y ≥ S have claim5 (n:ℕ) : y ≥ (a-b) n := E:Set RealhE:E.Nonemptyhbound:BddAbove E⊢ ∃ S, IsLUB E S E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |a n - a n'| ≤ 1 / (↑N + 1)claim3:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyS:Real := LIM aclaim4:S = LIM (a - b)y:Realhy:y ∈ upperBounds En:ℕhm2:y < ↑((a - b) n)⊢ ∃ n, ↑((a - b) n) ∈ upperBounds E E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |a n - a n'| ≤ 1 / (↑N + 1)claim3:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyS:Real := LIM aclaim4:S = LIM (a - b)y:Realhy:y ∈ upperBounds En:ℕhm2:y < ↑((a - b) n)⊢ ↑((a - b) n) ∈ upperBounds E All goals completed! 🐙 E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |a n - a n'| ≤ 1 / (↑N + 1)claim3:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyS:Real := LIM aclaim4:S = LIM (a - b)y:Realhy:y ∈ upperBounds Eclaim5:∀ (n : ℕ), y ≥ ↑((a - b) n)⊢ y ≥ LIM (a - b) E:Set RealhE:E.Nonemptyhbound:BddAbove Ex₀:Real := hE.somehx₀:x₀ ∈ Eclaim1:∀ (n : ℕ), ∃! m, ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds Em:ℕ → ℤ := fun n => ⋯.choosea:ℕ → ℚ := fun n => ↑(m n) / (↑n + 1)b:ℕ → ℚ := fun n => 1 / (↑n + 1)hb:{ n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchyhm1:∀ (n : ℕ), ↑(a n) ∈ upperBounds Ehm2:∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds Eclaim2:∀ (N n : ℕ), n ≥ N → ∀ n' ≥ N, |a n - a n'| ≤ 1 / (↑N + 1)claim3:{ n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchyS:Real := LIM aclaim4:S = LIM (a - b)y:Realhy:y ∈ upperBounds Eclaim5:∀ (n : ℕ), y ≥ ↑((a - b) n)⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then (a - b) n.toNat else 0, vanish := ⋯ }.isCauchy All goals completed! 🐙

A bare-bones extended real class to define supremum.

inductive ExtendedReal where | neg_infty : ExtendedReal | real (x:Real) : ExtendedReal | infty : ExtendedReal

Mathlib prefers ⊤ to denote the +∞ element.

instance ExtendedReal.inst_Top : Top ExtendedReal where top := infty

Mathlib prefers ⊥ to denote the -∞ element.

instance ExtendedReal.inst_Bot: Bot ExtendedReal where bot := infty
instance ExtendedReal.coe_real : Coe Real ExtendedReal where coe x := ExtendedReal.real xinstance ExtendedReal.real_coe : Coe ExtendedReal Real where coe X := match X with | neg_infty => 0 | real x => x | infty => 0abbrev ExtendedReal.is_finite (X : ExtendedReal) : Prop := match X with | neg_infty => False | real _ => True | infty => Falsetheorem ExtendedReal.finite_eq_coe {X: ExtendedReal} (hX: X.is_finite) : X = ((X:Real):ExtendedReal) := X:ExtendedRealhX:X.is_finite⊢ X = real (match X with | neg_infty => 0 | real x => x | infty => 0) hX:neg_infty.is_finite⊢ neg_infty = real (match neg_infty with | neg_infty => 0 | real x => x | infty => 0)x✝:RealhX:(real x✝).is_finite⊢ real x✝ = real (match real x✝ with | neg_infty => 0 | real x => x | infty => 0)hX:infty.is_finite⊢ infty = real (match infty with | neg_infty => 0 | real x => x | infty => 0) hX:neg_infty.is_finite⊢ neg_infty = real (match neg_infty with | neg_infty => 0 | real x => x | infty => 0) All goals completed! 🐙 x✝:RealhX:(real x✝).is_finite⊢ real x✝ = real (match real x✝ with | neg_infty => 0 | real x => x | infty => 0) All goals completed! 🐙 All goals completed! 🐙open Classical in /-- Визначення 5.5.10 (Supremum)-/ noncomputable abbrev ExtendedReal.sup (E: Set Real) : ExtendedReal := dite E.Nonempty (fun h1 ↦ dite (BddAbove E) (fun h2 ↦ ((Real.LUB_exist h1 h2).choose:Real)) (fun _ ↦ ⊤)) (fun _ ↦ ⊥)

Визначення 5.5.10 (Supremum)

theorem ExtendedReal.sup_of_empty : sup ∅ = ⊥ := ⊢ sup ∅ = ⊥ All goals completed! 🐙

Визначення 5.5.10 (Supremum)

theorem ExtendedReal.sup_of_unbounded {E: Set Real} (hb: ¬ BddAbove E) : sup E = ⊤ := E:Set Realhb:¬BddAbove E⊢ sup E = ⊤ have hE : E.Nonempty := E:Set Realhb:¬BddAbove E⊢ sup E = ⊤ E:Set Realhb:E = ∅⊢ BddAbove E All goals completed! 🐙 All goals completed! 🐙

Визначення 5.5.10 (Supremum)

theorem ExtendedReal.sup_of_bounded {E: Set Real} (hnon: E.Nonempty) (hb: BddAbove E) : IsLUB E (sup E) := E:Set Realhnon:E.Nonemptyhb:BddAbove E⊢ IsLUB E (match sup E with | neg_infty => 0 | real x => x | infty => 0) E:Set Realhnon:E.Nonemptyhb:BddAbove E⊢ IsLUB E ⋯.choose All goals completed! 🐙
theorem ExtendedReal.sup_of_bounded_finite {E: Set Real} (hnon: E.Nonempty) (hb: BddAbove E) : (sup E).is_finite := E:Set Realhnon:E.Nonemptyhb:BddAbove E⊢ (sup E).is_finite All goals completed! 🐙

Твердження 5.5.12

theorem declaration uses 'sorry'Real.exist_sqrt_two : ∃ x:Real, x^2 = 2 := ⊢ ∃ x, x ^ 2 = 2 -- цей доказ написан так, щоб співпадати із структурою орігінального тексту. E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}⊢ ∃ x, x ^ 2 = 2 have claim1: 2 ∈ upperBounds E := ⊢ ∃ x, x ^ 2 = 2 E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}⊢ ∀ x ∈ E, x ≤ 2 E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}y:Realhy:y ∈ E⊢ y ≤ 2 E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}y:Realhy:0 ≤ y ∧ y ^ 2 < 2⊢ y ≤ 2 E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}y:Realhy:2 < y⊢ 0 ≤ y → 2 ≤ y ^ 2 E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}y:Realhy:2 < yhpos:0 ≤ y⊢ 2 ≤ y ^ 2 calc _ ≤ 2 * 2 := E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}y:Realhy:2 < yhpos:0 ≤ y⊢ 2 ≤ 2 * 2 All goals completed! 🐙 _ ≤ y * y := E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}y:Realhy:2 < yhpos:0 ≤ y⊢ 2 * 2 ≤ y * y All goals completed! 🐙 _ = y^2 := E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}y:Realhy:2 < yhpos:0 ≤ y⊢ y * y = y ^ 2 All goals completed! 🐙 have claim1' : BddAbove E := ⊢ ∃ x, x ^ 2 = 2 E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds E⊢ ∃ M, M ∈ upperBounds E; All goals completed! 🐙 have claim2: 1 ∈ E := ⊢ ∃ x, x ^ 2 = 2 All goals completed! 🐙 E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonempty⊢ ∃ x, x ^ 2 = 2 E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0⊢ ∃ x, x ^ 2 = 2 E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:IsLUB E x⊢ ∃ x, x ^ 2 = 2 have claim4 : x ≥ 1 := ⊢ ∃ x, x ^ 2 = 2 E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:x ∈ upperBounds E ∧ ∀ M' ∈ upperBounds E, M' ≥ x⊢ x ≥ 1 E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:x ∈ upperBounds E⊢ x ≥ 1 E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:∀ x_1 ∈ E, x_1 ≤ x⊢ x ≥ 1 All goals completed! 🐙 have claim5 : x ≤ 2 := ⊢ ∃ x, x ^ 2 = 2 E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:x ∈ upperBounds E ∧ ∀ M' ∈ upperBounds E, M' ≥ xclaim4:x ≥ 1⊢ x ≤ 2 All goals completed! 🐙 have claim6 : x.isPos := ⊢ ∃ x, x ^ 2 = 2 E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2⊢ x > 0; All goals completed! 🐙 E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.isPos⊢ x ^ 2 = 2 E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.isPosh:x ^ 2 > 2⊢ x ^ 2 = 2E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.isPosh:x ^ 2 < 2⊢ x ^ 2 = 2E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.isPosh:x ^ 2 = 2⊢ x ^ 2 = 2 E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.isPosh:x ^ 2 > 2⊢ x ^ 2 = 2 have claim11: ∃ ε, 0 < ε ∧ ε < 1 ∧ x^2 - 4*ε > 2 := ⊢ ∃ x, x ^ 2 = 2 E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.isPosh:x ^ 2 > 2ε:Real := min (1 / 2) ((x ^ 2 - 2) / 8)⊢ ∃ ε, 0 < ε ∧ ε < 1 ∧ x ^ 2 - 4 * ε > 2 have hx : x^2 - 2 > 0 := ⊢ ∃ x, x ^ 2 = 2 All goals completed! 🐙 have hε : 0 < ε := ⊢ ∃ x, x ^ 2 = 2 All goals completed! 🐙 E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.isPosh:x ^ 2 > 2ε:Real := min (1 / 2) ((x ^ 2 - 2) / 8)hx:x ^ 2 - 2 > 0hε:0 < εhε1:ε ≤ 1 / 2⊢ ∃ ε, 0 < ε ∧ ε < 1 ∧ x ^ 2 - 4 * ε > 2 E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.isPosh:x ^ 2 > 2ε:Real := min (1 / 2) ((x ^ 2 - 2) / 8)hx:x ^ 2 - 2 > 0hε:0 < εhε1:ε ≤ 1 / 2hε2:ε ≤ (x ^ 2 - 2) / 8⊢ ∃ ε, 0 < ε ∧ ε < 1 ∧ x ^ 2 - 4 * ε > 2 exact ⟨ ε, hε, (E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.isPosh:x ^ 2 > 2ε:Real := min (1 / 2) ((x ^ 2 - 2) / 8)hx:x ^ 2 - 2 > 0hε:0 < εhε1:ε ≤ 1 / 2hε2:ε ≤ (x ^ 2 - 2) / 8⊢ ε < 1 All goals completed! 🐙), (E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.isPosh:x ^ 2 > 2ε:Real := min (1 / 2) ((x ^ 2 - 2) / 8)hx:x ^ 2 - 2 > 0hε:0 < εhε1:ε ≤ 1 / 2hε2:ε ≤ (x ^ 2 - 2) / 8⊢ x ^ 2 - 4 * ε > 2 All goals completed! 🐙) ⟩ E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.isPosh:x ^ 2 > 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 - 4 * ε > 2⊢ x ^ 2 = 2 have claim12: (x-ε)^2 > 2 := calc _ = x^2 - 2 * ε * x + ε * ε := E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.isPosh:x ^ 2 > 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 - 4 * ε > 2⊢ (x - ε) ^ 2 = x ^ 2 - 2 * ε * x + ε * ε All goals completed! 🐙 _ ≥ x^2 - 2 * ε * 2 + 0 * 0 := E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.isPosh:x ^ 2 > 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 - 4 * ε > 2⊢ x ^ 2 - 2 * ε * x + ε * ε ≥ x ^ 2 - 2 * ε * 2 + 0 * 0 All goals completed! 🐙 _ = x^2 - 4 * ε := E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.isPosh:x ^ 2 > 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 - 4 * ε > 2⊢ x ^ 2 - 2 * ε * 2 + 0 * 0 = x ^ 2 - 4 * ε All goals completed! 🐙 _ > 2 := hε3 have why (y:Real) (hy: y ∈ E) : x - ε ≥ y := ⊢ ∃ x, x ^ 2 = 2 All goals completed! 🐙 have claim13: x-ε ∈ upperBounds E := ⊢ ∃ x, x ^ 2 = 2 rwa [upperBound_defE:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.isPosh:x ^ 2 > 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 - 4 * ε > 2claim12:(x - ε) ^ 2 > 2why:∀ y ∈ E, x - ε ≥ y⊢ ∀ x_1 ∈ E, x_1 ≤ x - ε have claim14: x ≤ x-ε := ⊢ ∃ x, x ^ 2 = 2 E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:x ∈ upperBounds E ∧ ∀ M' ∈ upperBounds E, M' ≥ xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.isPosh:x ^ 2 > 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 - 4 * ε > 2claim12:(x - ε) ^ 2 > 2why:∀ y ∈ E, x - ε ≥ yclaim13:x - ε ∈ upperBounds E⊢ x ≤ x - ε All goals completed! 🐙 All goals completed! 🐙 E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.isPosh:x ^ 2 < 2⊢ x ^ 2 = 2 have claim7 : ∃ ε, 0 < ε ∧ ε < 1 ∧ x^2 + 5*ε < 2 := ⊢ ∃ x, x ^ 2 = 2 E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.isPosh:x ^ 2 < 2ε:Real := min (1 / 2) ((2 - x ^ 2) / 10)⊢ ∃ ε, 0 < ε ∧ ε < 1 ∧ x ^ 2 + 5 * ε < 2 have hx : 2 - x^2 > 0 := ⊢ ∃ x, x ^ 2 = 2 All goals completed! 🐙 have hε: 0 < ε := ⊢ ∃ x, x ^ 2 = 2 All goals completed! 🐙 E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.isPosh:x ^ 2 < 2ε:Real := min (1 / 2) ((2 - x ^ 2) / 10)hx:2 - x ^ 2 > 0hε:0 < εhε1:ε ≤ 1 / 2⊢ ∃ ε, 0 < ε ∧ ε < 1 ∧ x ^ 2 + 5 * ε < 2 E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.isPosh:x ^ 2 < 2ε:Real := min (1 / 2) ((2 - x ^ 2) / 10)hx:2 - x ^ 2 > 0hε:0 < εhε1:ε ≤ 1 / 2hε2:ε ≤ (2 - x ^ 2) / 10⊢ ∃ ε, 0 < ε ∧ ε < 1 ∧ x ^ 2 + 5 * ε < 2 exact ⟨ ε, hε, (E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.isPosh:x ^ 2 < 2ε:Real := min (1 / 2) ((2 - x ^ 2) / 10)hx:2 - x ^ 2 > 0hε:0 < εhε1:ε ≤ 1 / 2hε2:ε ≤ (2 - x ^ 2) / 10⊢ ε < 1 All goals completed! 🐙), (E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.isPosh:x ^ 2 < 2ε:Real := min (1 / 2) ((2 - x ^ 2) / 10)hx:2 - x ^ 2 > 0hε:0 < εhε1:ε ≤ 1 / 2hε2:ε ≤ (2 - x ^ 2) / 10⊢ x ^ 2 + 5 * ε < 2 All goals completed! 🐙) ⟩ E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.isPosh:x ^ 2 < 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 + 5 * ε < 2⊢ x ^ 2 = 2 have claim8 : (x+ε)^2 < 2 := calc _ = x^2 + (2*x)*ε + ε*ε := E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.isPosh:x ^ 2 < 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 + 5 * ε < 2⊢ (x + ε) ^ 2 = x ^ 2 + 2 * x * ε + ε * ε All goals completed! 🐙 _ ≤ x^2 + (2*2)*ε + 1*ε := E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.isPosh:x ^ 2 < 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 + 5 * ε < 2⊢ x ^ 2 + 2 * x * ε + ε * ε ≤ x ^ 2 + 2 * 2 * ε + 1 * ε All goals completed! 🐙 _ = x^2 + 5*ε := E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.isPosh:x ^ 2 < 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 + 5 * ε < 2⊢ x ^ 2 + 2 * 2 * ε + 1 * ε = x ^ 2 + 5 * ε All goals completed! 🐙 _ < 2 := hε3 have claim9 : x + ε ∈ E := ⊢ ∃ x, x ^ 2 = 2 E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:IsLUB E xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.isPosh:x ^ 2 < 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 + 5 * ε < 2claim8:(x + ε) ^ 2 < 2⊢ 0 ≤ x + ε; All goals completed! 🐙 have claim10 : x + ε ≤ x := ⊢ ∃ x, x ^ 2 = 2 E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim3:x ∈ upperBounds E ∧ ∀ M' ∈ upperBounds E, M' ≥ xclaim4:x ≥ 1claim5:x ≤ 2claim6:x.isPosh:x ^ 2 < 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 + 5 * ε < 2claim8:(x + ε) ^ 2 < 2claim9:x + ε ∈ E⊢ x + ε ≤ x E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim4:x ≥ 1claim5:x ≤ 2claim6:x.isPosh:x ^ 2 < 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 + 5 * ε < 2claim8:(x + ε) ^ 2 < 2claim9:x + ε ∈ Eclaim3:x ∈ upperBounds E⊢ x + ε ≤ x E:Set Real := {y | y ≥ 0 ∧ y ^ 2 < 2}claim1:2 ∈ upperBounds Eclaim1':BddAbove Eclaim2:1 ∈ Eclaim2':E.Nonemptyx:Real := match ExtendedReal.sup E with | ExtendedReal.neg_infty => 0 | ExtendedReal.real x => x | ExtendedReal.infty => 0claim4:x ≥ 1claim5:x ≤ 2claim6:x.isPosh:x ^ 2 < 2ε:Realhε1:0 < εhε2:ε < 1hε3:x ^ 2 + 5 * ε < 2claim8:(x + ε) ^ 2 < 2claim9:x + ε ∈ Eclaim3:∀ x_1 ∈ E, x_1 ≤ x⊢ x + ε ≤ x All goals completed! 🐙 All goals completed! 🐙 All goals completed! 🐙

Ремарка 5.5.13

theorem declaration uses 'sorry'Real.exist_irrational : ∃ x:Real, ¬ ∃ q:ℚ, x = (q:Real) := ⊢ ∃ x, ¬∃ q, x = ↑q All goals completed! 🐙
theorem declaration uses 'sorry'Real.GLB_exist {E: Set Real} (hE: Set.Nonempty E) (hbound: BddBelow E): ∃ S, IsGLB E S := E:Set RealhE:E.Nonemptyhbound:BddBelow E⊢ ∃ S, IsGLB E S All goals completed! 🐙open Classical in noncomputable abbrev ExtendedReal.inf (E: Set Real) : ExtendedReal := dite E.Nonempty (fun h1 ↦ dite (BddBelow E) (fun h2 ↦ ((Real.GLB_exist h1 h2).choose:Real)) (fun _ ↦ ⊥)) (fun _ ↦ ⊤)theorem ExtendedReal.inf_of_empty : inf ∅ = ⊤ := ⊢ inf ∅ = ⊤ All goals completed! 🐙theorem ExtendedReal.inf_of_unbounded {E: Set Real} (hb: ¬ BddBelow E) : inf E = ⊥ := E:Set Realhb:¬BddBelow E⊢ inf E = ⊥ have hE : E.Nonempty := E:Set Realhb:¬BddBelow E⊢ inf E = ⊥ E:Set Realhb:E = ∅⊢ BddBelow E All goals completed! 🐙 All goals completed! 🐙theorem ExtendedReal.inf_of_bounded {E: Set Real} (hnon: E.Nonempty) (hb: BddBelow E) : IsGLB E (inf E) := E:Set Realhnon:E.Nonemptyhb:BddBelow E⊢ IsGLB E (match inf E with | neg_infty => 0 | real x => x | infty => 0) E:Set Realhnon:E.Nonemptyhb:BddBelow E⊢ IsGLB E ⋯.choose All goals completed! 🐙theorem ExtendedReal.inf_of_bounded_finite {E: Set Real} (hnon: E.Nonempty) (hb: BddBelow E) : (inf E).is_finite := E:Set Realhnon:E.Nonemptyhb:BddBelow E⊢ (inf E).is_finite All goals completed! 🐙

Helper lemma for Exercise 5.5.1.

theorem Real.mem_neg (E: Set Real) (x:Real) : x ∈ -E ↔ -x ∈ E := Set.mem_neg

Вправа 5.5.1

theorem declaration uses 'sorry'Real.inf_neg {E: Set Real} {M:Real} (h: IsLUB E M) : IsGLB (-E) (-M) := E:Set RealM:Realh:IsLUB E M⊢ IsGLB (-E) (-M) All goals completed! 🐙

Вправа 5.5.5

theorem declaration uses 'sorry'Real.irrat_between {x y:Real} (hxy: x < y) : ∃ z, x < z ∧ z < y ∧ ¬ ∃ q:ℚ, z = (q:Real) := x:Realy:Realhxy:x < y⊢ ∃ z, x < z ∧ z < y ∧ ¬∃ q, z = ↑q All goals completed! 🐙
/- Use the notion of supremum in this section to define a Mathlib `sSup` operation -/ noncomputable instance Real.inst_SupSet : SupSet Real where sSup E := ((ExtendedReal.sup E):Real)

Use the SupSet.sSup.{u_1} {α : Type u_1} [self : SupSet α] : Set α → αsSup operation to build a conditionally complete lattice structure on Real : TypeReal

noncomputable instance Real.inst_conditionallyCompleteLattice : ConditionallyCompleteLattice Real := conditionallyCompleteLatticeOfsSup Real (fun _ _ ↦ Set.Finite.bddAbove (x✝¹:Realx✝:Real⊢ {x✝¹, x✝}.Finite All goals completed! 🐙)) (fun _ _ ↦ Set.Finite.bddBelow (x✝¹:Realx✝:Real⊢ {x✝¹, x✝}.Finite All goals completed! 🐙)) (⊢ ∀ (s : Set Real), BddAbove s → s.Nonempty → IsLUB s (sSup s) E:Set Realhbound:BddAbove Ehnon:E.Nonempty⊢ IsLUB E (sSup E); All goals completed! 🐙)
theorem ExtendedReal.sSup_of_bounded {E: Set Real} (hnon: E.Nonempty) (hb: BddAbove E) : IsLUB E (sSup E) := sup_of_bounded hnon hbend Chapter5