Ordering the reals
Аналіз I, Розділ 5.4: Впорядкування дійсних чисел
Я (пр.перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним рішенням Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підбуцнути", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.
Основні конструкції та результати цього розділу:
-
Порядок на дійсній прямій
Підказки від попередніх користувачів
Користувачі супровідного матеріалу, які виконали вправи в цьому розділі, можуть надсилати свої поради майбутнім користувачам цього розділу як PRи.
-
(Додайте підказку тут)
namespace Chapter5Визначення 5.4.1 (послідовності, обмежені від нуля з врахуванням знаку). Послідовності індексуються так, щоб починатися з нуля, оскільки це зручніше для цілей Mathlib.
abbrev BoundedAwayPos (a:ℕ → ℚ) : Prop :=
∃ (c:ℚ), c > 0 ∧ ∀ n, a n ≥ cВизначення 5.4.1 (послідовності, обмежені від нуля з врахуванням знаку).
abbrev BoundedAwayNeg (a:ℕ → ℚ) : Prop :=
∃ (c:ℚ), c > 0 ∧ ∀ n, a n ≤ -cВизначення 5.4.1 (послідовності, обмежені від нуля з врахуванням знаку).
theorem boundedAwayPos_def (a:ℕ → ℚ) : BoundedAwayPos a ↔ ∃ (c:ℚ), c > 0 ∧ ∀ n, a n ≥ c := a:ℕ → ℚ⊢ BoundedAwayPos a ↔ ∃ c > 0, ∀ (n : ℕ), a n ≥ c
All goals completed! 🐙Визначення 5.4.1 (послідовності, обмежені від нуля з врахуванням знаку).
theorem boundedAwayNeg_def (a:ℕ → ℚ) : BoundedAwayNeg a ↔ ∃ (c:ℚ), c > 0 ∧ ∀ n, a n ≤ -c := a:ℕ → ℚ⊢ BoundedAwayNeg a ↔ ∃ c > 0, ∀ (n : ℕ), a n ≤ -c
All goals completed! 🐙Приклади 5.4.2
example : BoundedAwayPos (fun n ↦ 1 + 10^(-(n:ℤ)-1)) := ⟨ 1, ⊢ 1 > 0 All goals completed! 🐙, ⊢ ∀ (n : ℕ), (fun n => 1 + 10 ^ (-↑n - 1)) n ≥ 1 n✝:ℕ⊢ (fun n => 1 + 10 ^ (-↑n - 1)) n✝ ≥ 1; n✝:ℕ⊢ 0 ≤ 10 ^ (-↑n✝ - 1); All goals completed! 🐙 ⟩Приклади 5.4.2
example : BoundedAwayNeg (fun n ↦ -1 - 10^(-(n:ℤ)-1)) := ⟨ 1, ⊢ 1 > 0 All goals completed! 🐙, ⊢ ∀ (n : ℕ), (fun n => -1 - 10 ^ (-↑n - 1)) n ≤ -1 n✝:ℕ⊢ (fun n => -1 - 10 ^ (-↑n - 1)) n✝ ≤ -1; n✝:ℕ⊢ 0 ≤ 10 ^ (-↑n✝ - 1); All goals completed! 🐙 ⟩Приклади 5.4.2
example : ¬ BoundedAwayPos (fun n ↦ (-1)^n) := ⊢ ¬BoundedAwayPos fun n => (-1) ^ n
c:ℚh1:c > 0h2:∀ (n : ℕ), (fun n => (-1) ^ n) n ≥ c⊢ False; c:ℚh1:c > 0h2:(fun n => (-1) ^ n) 1 ≥ c⊢ False; All goals completed! 🐙Приклади 5.4.2
example : ¬ BoundedAwayNeg (fun n ↦ (-1)^n) := ⊢ ¬BoundedAwayNeg fun n => (-1) ^ n
c:ℚh1:c > 0h2:∀ (n : ℕ), (fun n => (-1) ^ n) n ≤ -c⊢ False; c:ℚh1:c > 0h2:(fun n => (-1) ^ n) 0 ≤ -c⊢ False; All goals completed! 🐙Приклади 5.4.2
example : BoundedAwayZero (fun n ↦ (-1)^n) := ⟨ 1, ⊢ 1 > 0 All goals completed! 🐙, ⊢ ∀ (n : ℕ), |(fun n => (-1) ^ n) n| ≥ 1 n✝:ℕ⊢ |(fun n => (-1) ^ n) n✝| ≥ 1; All goals completed! 🐙 ⟩theorem BoundedAwayZero.boundedAwayPos {a:ℕ → ℚ} (ha: BoundedAwayPos a) : BoundedAwayZero a := a:ℕ → ℚha:BoundedAwayPos a⊢ BoundedAwayZero a
a:ℕ → ℚha:BoundedAwayPos ac:ℚh1:c > 0n:ℕh2:a n ≥ c⊢ |a n| ≥ c; rwa [abs_of_nonneg (a:ℕ → ℚha:BoundedAwayPos ac:ℚh1:c > 0n:ℕh2:a n ≥ c⊢ 0 ≤ a n All goals completed! 🐙)a:ℕ → ℚha:BoundedAwayPos ac:ℚh1:c > 0n:ℕh2:a n ≥ c⊢ a n ≥ ctheorem BoundedAwayZero.boundedAwayNeg {a:ℕ → ℚ} (ha: BoundedAwayNeg a) : BoundedAwayZero a := a:ℕ → ℚha:BoundedAwayNeg a⊢ BoundedAwayZero a
a:ℕ → ℚha:BoundedAwayNeg ac:ℚh1:c > 0n:ℕh2:a n ≤ -c⊢ |a n| ≥ c; a:ℕ → ℚha:BoundedAwayNeg ac:ℚh1:c > 0n:ℕh2:a n ≤ -c⊢ -a n ≥ c; All goals completed! 🐙theorem not_boundedAwayPos_boundedAwayNeg {a:ℕ → ℚ} : ¬ (BoundedAwayPos a ∧ BoundedAwayNeg a) := a:ℕ → ℚ⊢ ¬(BoundedAwayPos a ∧ BoundedAwayNeg a)
a:ℕ → ℚw✝¹:ℚleft✝¹:w✝¹ > 0h2:∀ (n : ℕ), a n ≥ w✝¹w✝:ℚleft✝:w✝ > 0h4:∀ (n : ℕ), a n ≤ -w✝⊢ False; All goals completed! 🐙abbrev Real.IsPos (x:Real) : Prop :=
∃ a:ℕ → ℚ, BoundedAwayPos a ∧ (a:Sequence).IsCauchy ∧ x = LIM aabbrev Real.IsNeg (x:Real) : Prop :=
∃ a:ℕ → ℚ, BoundedAwayNeg a ∧ (a:Sequence).IsCauchy ∧ x = LIM atheorem Real.isPos_def (x:Real) :
IsPos x ↔ ∃ a:ℕ → ℚ, BoundedAwayPos a ∧ (a:Sequence).IsCauchy ∧ x = LIM a := x:Real⊢ x.IsPos ↔ ∃ a, BoundedAwayPos a ∧ (↑a).IsCauchy ∧ x = LIM a All goals completed! 🐙theorem Real.isNeg_def (x:Real) :
IsNeg x ↔ ∃ a:ℕ → ℚ, BoundedAwayNeg a ∧ (a:Sequence).IsCauchy ∧ x = LIM a := x:Real⊢ x.IsNeg ↔ ∃ a, BoundedAwayNeg a ∧ (↑a).IsCauchy ∧ x = LIM a All goals completed! 🐙Твердження 5.4.4 (базові властивості додатних дійсних чисел) / Вправа 5.4.1
theorem Real.trichotomous (x:Real) : x = 0 ∨ x.IsPos ∨ x.IsNeg := x:Real⊢ x = 0 ∨ x.IsPos ∨ x.IsNeg All goals completed! 🐙Твердження 5.4.4 (базові властивості додатних дійсних чисел) / Вправа 5.4.1
theorem Real.not_zero_pos (x:Real) : ¬(x = 0 ∧ x.IsPos) := x:Real⊢ ¬(x = 0 ∧ x.IsPos) All goals completed! 🐙theorem Real.nonzero_of_pos {x:Real} (hx: x.IsPos) : x ≠ 0 := x:Realhx:x.IsPos⊢ x ≠ 0
x:Realhx:x.IsPosthis:?_mvar.15897 := Chapter5.Real.not_zero_pos _fvar.15893⊢ x ≠ 0
All goals completed! 🐙Твердження 5.4.4 (базові властивості додатних дійсних чисел) / Вправа 5.4.1
theorem Real.not_zero_neg (x:Real) : ¬(x = 0 ∧ x.IsNeg) := x:Real⊢ ¬(x = 0 ∧ x.IsNeg) All goals completed! 🐙theorem Real.nonzero_of_neg {x:Real} (hx: x.IsNeg) : x ≠ 0 := x:Realhx:x.IsNeg⊢ x ≠ 0
x:Realhx:x.IsNegthis:?_mvar.16366 := Chapter5.Real.not_zero_neg _fvar.16362⊢ x ≠ 0
All goals completed! 🐙Твердження 5.4.4 (базові властивості додатних дійсних чисел) / Вправа 5.4.1
theorem Real.not_pos_neg (x:Real) : ¬(x.IsPos ∧ x.IsNeg) := x:Real⊢ ¬(x.IsPos ∧ x.IsNeg) All goals completed! 🐙Твердження 5.4.4 (базові властивості додатних дійсних чисел) / Вправа 5.4.1
@[simp]
theorem Real.neg_iff_pos_of_neg (x:Real) : x.IsNeg ↔ (-x).IsPos := x:Real⊢ x.IsNeg ↔ (-x).IsPos All goals completed! 🐙Твердження 5.4.4 (базові властивості додатних дійсних чисел) / Вправа 5.4.1
theorem Real.pos_add {x y:Real} (hx: x.IsPos) (hy: y.IsPos) : (x+y).IsPos := x:Realy:Realhx:x.IsPoshy:y.IsPos⊢ (x + y).IsPos All goals completed! 🐙Твердження 5.4.4 (базові властивості додатних дійсних чисел) / Вправа 5.4.1
theorem Real.pos_mul {x y:Real} (hx: x.IsPos) (hy: y.IsPos) : (x*y).IsPos := x:Realy:Realhx:x.IsPoshy:y.IsPos⊢ (x * y).IsPos All goals completed! 🐙theorem Real.pos_of_coe (q:ℚ) : (q:Real).IsPos ↔ q > 0 := q:ℚ⊢ (↑q).IsPos ↔ q > 0 All goals completed! 🐙theorem Real.neg_of_coe (q:ℚ) : (q:Real).IsNeg ↔ q < 0 := q:ℚ⊢ (↑q).IsNeg ↔ q < 0 All goals completed! 🐙open Classical in
/-- Тут потрібно використовувати класичну логіку, оскільки isPos і isNeg не є вирішуваними. -/
noncomputable abbrev Real.abs (x:Real) : Real := if x.IsPos then x else (if x.IsNeg then -x else 0)Визначення 5.4.5 (модуль)
@[simp]
theorem Real.abs_of_pos (x:Real) (hx: x.IsPos) : abs x = x := x:Realhx:x.IsPos⊢ x.abs = x
All goals completed! 🐙Визначення 5.4.5 (модуль)
@[simp]
theorem Real.abs_of_neg (x:Real) (hx: x.IsNeg) : abs x = -x := x:Realhx:x.IsNeg⊢ x.abs = -x
have : ¬x.IsPos := x:Realhx:x.IsNeg⊢ x.abs = -x x:Realhx:x.IsNegthis:?_mvar.22500 := Chapter5.Real.not_pos_neg _fvar.22489⊢ ¬x.IsPos; All goals completed! 🐙
All goals completed! 🐙Визначення 5.4.5 (модуль)
@[simp]
theorem Real.abs_of_zero : abs 0 = 0 := ⊢ abs 0 = 0
have hpos: ¬(0:Real).IsPos := ⊢ abs 0 = 0 this:?_mvar.259693 := Chapter5.Real.not_zero_pos 0⊢ ¬IsPos 0; All goals completed! 🐙
have hneg: ¬(0:Real).IsNeg := ⊢ abs 0 = 0 hpos:¬Chapter5.Real.IsPos 0 := ?_mvar.259687this:?_mvar.496262 := Chapter5.Real.not_zero_neg 0⊢ ¬IsNeg 0; All goals completed! 🐙
All goals completed! 🐙Визначення 5.4.6 (Упорядкування дійсних чисел)
instance Real.instLT : LT Real where
lt x y := (x-y).IsNegВизначення 5.4.6 (Упорядкування дійсних чисел)
instance Real.instLE : LE Real where
le x y := (x < y) ∨ (x = y)theorem Real.lt_iff (x y:Real) : x < y ↔ (x-y).IsNeg := x:Realy:Real⊢ x < y ↔ (x - y).IsNeg All goals completed! 🐙theorem Real.le_iff (x y:Real) : x ≤ y ↔ (x < y) ∨ (x = y) := x:Realy:Real⊢ x ≤ y ↔ x < y ∨ x = y All goals completed! 🐙theorem Real.gt_iff (x y:Real) : x > y ↔ (x-y).IsPos := x:Realy:Real⊢ x > y ↔ (x - y).IsPos All goals completed! 🐙theorem Real.ge_iff (x y:Real) : x ≥ y ↔ (x > y) ∨ (x = y) := x:Realy:Real⊢ x ≥ y ↔ x > y ∨ x = y All goals completed! 🐙theorem Real.lt_of_coe (q q':ℚ): q < q' ↔ (q:Real) < (q':Real) := q:ℚq':ℚ⊢ q < q' ↔ ↑q < ↑q' All goals completed! 🐙theorem Real.gt_of_coe (q q':ℚ): q > q' ↔ (q:Real) > (q':Real) := Real.lt_of_coe _ _theorem Real.isPos_iff (x:Real) : x.IsPos ↔ x > 0 := x:Real⊢ x.IsPos ↔ x > 0 All goals completed! 🐙theorem Real.isNeg_iff (x:Real) : x.IsNeg ↔ x < 0 := x:Real⊢ x.IsNeg ↔ x < 0 All goals completed! 🐙Твердження 5.4.7(a) (трихотомія порядку) / Вправа 5.4.2
theorem Real.trichotomous' (x y:Real) : x > y ∨ x < y ∨ x = y := x:Realy:Real⊢ x > y ∨ x < y ∨ x = y All goals completed! 🐙Твердження 5.4.7(a) (трихотомія порядку) / Вправа 5.4.2
theorem Real.not_gt_and_lt (x y:Real) : ¬ (x > y ∧ x < y):= x:Realy:Real⊢ ¬(x > y ∧ x < y) All goals completed! 🐙Твердження 5.4.7(a) (трихотомія порядку) / Вправа 5.4.2
theorem Real.not_gt_and_eq (x y:Real) : ¬ (x > y ∧ x = y):= x:Realy:Real⊢ ¬(x > y ∧ x = y) All goals completed! 🐙Твердження 5.4.7(a) (трихотомія порядку) / Вправа 5.4.2
theorem Real.not_lt_and_eq (x y:Real) : ¬ (x < y ∧ x = y):= x:Realy:Real⊢ ¬(x < y ∧ x = y) All goals completed! 🐙Твердження 5.4.7(b) (порядок є антисиметричним) / Вправа 5.4.2
theorem Real.antisymm (x y:Real) : x < y ↔ y > x := x:Realy:Real⊢ x < y ↔ y > x All goals completed! 🐙Твердження 5.4.7(c) (порядок є транзитивним) / Вправа 5.4.2
theorem Real.lt_trans {x y z:Real} (hxy: x < y) (hyz: y < z) : x < z := x:Realy:Realz:Realhxy:x < yhyz:y < z⊢ x < z All goals completed! 🐙Твердження 5.4.7(d) (додавання зберігає порядок) / Вправа 5.4.2
theorem Real.add_lt_add_right {x y:Real} (z:Real) (hxy: x < y) : x + z < y + z := x:Realy:Realz:Realhxy:x < y⊢ x + z < y + z All goals completed! 🐙Твердження 5.4.7(e) (множення на додатне число зберігає порядок) / Вправа 5.4.2
theorem Real.mul_lt_mul_right {x y z:Real} (hxy: x < y) (hz: z.IsPos) : x * z < y * z := x:Realy:Realz:Realhxy:x < yhz:z.IsPos⊢ x * z < y * z
x:Realy:Realz:Realhxy:(y - x).IsPoshz:z.IsPos⊢ (y * z - x * z).IsPos; x:Realy:Realz:Realhxy:(y - x).IsPoshz:z.IsPos⊢ y * z - x * z = (y - x) * z; All goals completed! 🐙Твердження 5.4.7(e) (множення на додатне число зберігає порядок) / Вправа 5.4.2
theorem Real.mul_le_mul_left {x y z:Real} (hxy: x ≤ y) (hz: z.IsPos) : z * x ≤ z * y := x:Realy:Realz:Realhxy:x ≤ yhz:z.IsPos⊢ z * x ≤ z * y All goals completed! 🐙theorem Real.mul_pos_neg {x y:Real} (hx: x.IsPos) (hy: y.IsNeg) : (x * y).IsNeg := x:Realy:Realhx:x.IsPoshy:y.IsNeg⊢ (x * y).IsNeg
All goals completed! 🐙open Classical in
/--
(Не в підручнику) Дійсні числа мають структуру лінійного впорядкування. Це впорядкування не є обчислюваним,
тому для забезпечення розв'язності необхідна класична логіка.
-/
noncomputable instance Real.instLinearOrder : LinearOrder Real where
le_refl := sorry
le_trans := sorry
lt_iff_le_not_ge := sorry
le_antisymm := sorry
le_total := sorry
toDecidableLE := Classical.decRel _(Не в підручнику) Лінійні впорядкування включають визначення абсолютного значення |·|. Покажіть, що воно збігається з нашим попереднім визначенням.
theorem Real.abs_eq_abs (x:Real) : |x| = abs x := x:Real⊢ |x| = x.abs All goals completed! 🐙Твердження 5.4.8
theorem Real.inv_of_pos {x:Real} (hx: x.IsPos) : x⁻¹.IsPos := x:Realhx:x.IsPos⊢ x⁻¹.IsPos
x:Realhx:x.IsPoshnon:x ≠ 0⊢ x⁻¹.IsPos
x:Realhx:x.IsPoshnon:x ≠ 0hident:x⁻¹ * x = 1⊢ x⁻¹.IsPos
have hinv_non: x⁻¹ ≠ 0 := x:Realhx:x.IsPos⊢ x⁻¹.IsPos x:Realhx:x.IsPoshnon:x ≠ 0hident:x⁻¹ = 0⊢ x⁻¹ * x ≠ 1; All goals completed! 🐙
have hnonneg : ¬x⁻¹.IsNeg := x:Realhx:x.IsPos⊢ x⁻¹.IsPos
x:Realhx:x.IsPoshnon:x ≠ 0hident:x⁻¹ * x = 1hinv_non:_fvar.740976⁻¹ ≠ 0 := ?_mvar.793412h:x⁻¹.IsNeg⊢ False
x:Realhx:x.IsPoshnon:x ≠ 0hident:x⁻¹ * x = 1hinv_non:_fvar.740976⁻¹ ≠ 0 := ?_mvar.793412h:x⁻¹.IsNegthis:(x * x⁻¹).IsNeg⊢ False
have id : -(1:Real) = (-1:ℚ) := x:Realhx:x.IsPos⊢ x⁻¹.IsPos All goals completed! 🐙
x:Realhx:x.IsPoshnon:x ≠ 0hident:x⁻¹ * x = 1hinv_non:_fvar.740976⁻¹ ≠ 0 := ?_mvar.793412h:x⁻¹.IsNegid:-1 = ↑(-1) := ?_mvar.802697this:-1 > 0⊢ False
All goals completed! 🐙
x:Realhx:x.IsPoshnon:x ≠ 0hident:x⁻¹ * x = 1hinv_non:_fvar.740976⁻¹ ≠ 0 := ?_mvar.793412hnonneg:¬Chapter5.Real.IsNeg _fvar.740976⁻¹ := ?_mvar.794603trich:?_mvar.804167 := Chapter5.Real.trichotomous _fvar.740976⁻¹⊢ x⁻¹.IsPos
All goals completed! 🐙theorem Real.div_of_pos {x y:Real} (hx: x.IsPos) (hy: y.IsPos) : (x/y).IsPos := x:Realy:Realhx:x.IsPoshy:y.IsPos⊢ (x / y).IsPos All goals completed! 🐙theorem Real.inv_of_gt {x y:Real} (hx: x.IsPos) (hy: y.IsPos) (hxy: x > y) : x⁻¹ < y⁻¹ := x:Realy:Realhx:x.IsPoshy:y.IsPoshxy:x > y⊢ x⁻¹ < y⁻¹
x:Realy:Realhx:x.IsPoshy:y.IsPoshxy:x > yhxnon:x ≠ 0⊢ x⁻¹ < y⁻¹
x:Realy:Realhx:x.IsPoshy:y.IsPoshxy:x > yhxnon:x ≠ 0hynon:y ≠ 0⊢ x⁻¹ < y⁻¹
x:Realy:Realhx:x.IsPoshy:y.IsPoshxy:x > yhxnon:x ≠ 0hynon:y ≠ 0hxinv:x⁻¹.IsPos⊢ x⁻¹ < y⁻¹
x:Realy:Realhx:x.IsPoshy:y.IsPoshxy:x > yhxnon:x ≠ 0hynon:y ≠ 0hxinv:x⁻¹.IsPosthis:y⁻¹ ≤ x⁻¹⊢ False
x:Realy:Realhx:x.IsPoshy:y.IsPoshxy:x > yhxnon:x ≠ 0hynon:y ≠ 0hxinv:x⁻¹.IsPosthis✝:y⁻¹ ≤ x⁻¹this:1 > 1 := Trans.trans (Trans.trans (Trans.trans ⋯ ⋯) ⋯) ⋯⊢ False
All goals completed! 🐙(Не в підручнику) Дійсні числа мають структуру строго впорядкованого кільця.
instance Real.instIsStrictOrderedRing : IsStrictOrderedRing Real where
add_le_add_left := ⊢ ∀ (a b : Real), a ≤ b → ∀ (c : Real), c + a ≤ c + b All goals completed! 🐙
add_le_add_right := ⊢ ∀ (a b : Real), a ≤ b → ∀ (c : Real), a + c ≤ b + c All goals completed! 🐙
mul_lt_mul_of_pos_left := ⊢ ∀ (a b c : Real), a < b → 0 < c → c * a < c * b All goals completed! 🐙
mul_lt_mul_of_pos_right := ⊢ ∀ (a b c : Real), a < b → 0 < c → a * c < b * c All goals completed! 🐙
le_of_add_le_add_left := ⊢ ∀ (a b c : Real), a + b ≤ a + c → b ≤ c All goals completed! 🐙
zero_le_one := ⊢ 0 ≤ 1 All goals completed! 🐙Твердження 5.4.9 (Невід'ємні дійсні числа утворюють замкнену множину.)
theorem Real.LIM_of_nonneg {a: ℕ → ℚ} (ha: ∀ n, a n ≥ 0) (hcauchy: (a:Sequence).IsCauchy) :
LIM a ≥ 0 := a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchy⊢ LIM a ≥ 0
-- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyhlim:LIM a < 0⊢ False
a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811220hlim:x < 0⊢ False
a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811220hlim:∃ a, BoundedAwayNeg a ∧ (↑a).IsCauchy ∧ x = LIM a⊢ False; a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811220b:ℕ → ℚhb:BoundedAwayNeg bhb_cauchy:(↑b).IsCauchyhlim:x = LIM b⊢ False
a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811220b:ℕ → ℚhb:∃ c > 0, ∀ (n : ℕ), b n ≤ -chb_cauchy:(↑b).IsCauchyhlim:x = LIM b⊢ False; a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811220b:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0hb:∀ (n : ℕ), b n ≤ -c⊢ False
have claim1 : ∀ n, ¬ (c/2).Close (a n) (b n) := a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchy⊢ LIM a ≥ 0
a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811220b:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0hb:∀ (n : ℕ), b n ≤ -cn:ℕ⊢ ¬(c / 2).Close (a n) (b n); a:ℕ → ℚhcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811220b:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0hb:∀ (n : ℕ), b n ≤ -cn:ℕha:a n ≥ 0⊢ ¬(c / 2).Close (a n) (b n); a:ℕ → ℚhcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811220b:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0n:ℕha:a n ≥ 0hb:b n ≤ -c⊢ ¬(c / 2).Close (a n) (b n)
a:ℕ → ℚhcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811220b:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0n:ℕha:a n ≥ 0hb:b n ≤ -c⊢ c / 2 < |a n - b n|
calc
_ < c := a:ℕ → ℚhcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811220b:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0n:ℕha:a n ≥ 0hb:b n ≤ -c⊢ c / 2 < c All goals completed! 🐙
_ ≤ a n - b n := a:ℕ → ℚhcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811220b:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0n:ℕha:a n ≥ 0hb:b n ≤ -c⊢ c ≤ a n - b n All goals completed! 🐙
_ ≤ _ := le_abs_self _
have claim2 : ¬(c/2).EventuallyClose (a:Sequence) (b:Sequence) := a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchy⊢ LIM a ≥ 0
a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811220b:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0hb:∀ (n : ℕ), b n ≤ -cclaim1:(c / 2).EventuallyClose ↑a ↑b⊢ ∃ n, (c / 2).Close (a n) (b n); a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811220b:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0hb:∀ (n : ℕ), b n ≤ -cclaim1:∃ N, ∀ n ≥ N, |a n - b n| ≤ c / 2⊢ ∃ n, (c / 2).Close (a n) (b n); a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811220b:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0hb:∀ (n : ℕ), b n ≤ -cclaim1✝:∃ N, ∀ n ≥ N, |a n - b n| ≤ c / 2N:ℕclaim1:∀ n ≥ N, |a n - b n| ≤ c / 2⊢ (c / 2).Close (a N) (b N); All goals completed! 🐙
have claim3 : ¬Sequence.Equiv a b := a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchy⊢ LIM a ≥ 0 a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811220b:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0hb:∀ (n : ℕ), b n ≤ -cclaim1:∀ (n : ℕ), ¬(_fvar.811901 / 2).Close (@_fvar.811220 n) (@_fvar.811845 n) := ?_mvar.812002claim2:Sequence.Equiv a b⊢ (c / 2).EventuallyClose ↑a ↑b; a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811220b:ℕ → ℚhb_cauchy:(↑b).IsCauchyhlim:x = LIM bc:ℚcpos:c > 0hb:∀ (n : ℕ), b n ≤ -cclaim1:∀ (n : ℕ), ¬(_fvar.811901 / 2).Close (@_fvar.811220 n) (@_fvar.811845 n) := ?_mvar.812002claim2:∀ ε > 0, ε.EventuallyClose ↑a ↑b⊢ (c / 2).EventuallyClose ↑a ↑b; All goals completed! 🐙
a:ℕ → ℚha:∀ (n : ℕ), a n ≥ 0hcauchy:(↑a).IsCauchyx:Chapter5.Real := Chapter5.LIM _fvar.811220b:ℕ → ℚhb_cauchy:(↑b).IsCauchyc:ℚcpos:c > 0hb:∀ (n : ℕ), b n ≤ -cclaim1:∀ (n : ℕ), ¬(_fvar.811901 / 2).Close (@_fvar.811220 n) (@_fvar.811845 n) := ?_mvar.812002claim2:¬Rat.EventuallyClose (_fvar.811901 / 2) ↑_fvar.811220 ↑_fvar.811845 := ?_mvar.815053claim3:¬Chapter5.Sequence.Equiv _fvar.811220 _fvar.811845 := ?_mvar.827451hlim:Sequence.Equiv a b⊢ False
All goals completed! 🐙Наслідок 5.4.10
theorem Real.LIM_mono {a b:ℕ → ℚ} (ha: (a:Sequence).IsCauchy) (hb: (b:Sequence).IsCauchy)
(hmono: ∀ n, a n ≤ b n) :
LIM a ≤ LIM b := a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchyhmono:∀ (n : ℕ), a n ≤ b n⊢ LIM a ≤ LIM b
-- Доведення написане так, щоб відповідати структурі оригінального тексту.
have := LIM_of_nonneg (a := b - a) (a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchyhmono:∀ (n : ℕ), a n ≤ b n⊢ ∀ (n : ℕ), (b - a) n ≥ 0 a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchyhmono:∀ (n : ℕ), a n ≤ b nn:ℕ⊢ (b - a) n ≥ 0; All goals completed! 🐙) (Sequence.IsCauchy.sub hb ha)
a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchyhmono:∀ (n : ℕ), a n ≤ b nthis:LIM b - LIM a ≥ 0⊢ LIM a ≤ LIM b; All goals completed! 🐙Ремарка 5.4.11 -
theorem Real.LIM_mono_fail :
∃ (a b:ℕ → ℚ), (a:Sequence).IsCauchy
∧ (b:Sequence).IsCauchy
∧ (∀ n, a n > b n)
∧ ¬LIM a > LIM b := ⊢ ∃ a b, (↑a).IsCauchy ∧ (↑b).IsCauchy ∧ (∀ (n : ℕ), a n > b n) ∧ ¬LIM a > LIM b
⊢ ∃ b,
(↑fun n => 1 + 1 / (↑n + 1)).IsCauchy ∧
(↑b).IsCauchy ∧ (∀ (n : ℕ), (fun n => 1 + 1 / (↑n + 1)) n > b n) ∧ ¬(LIM fun n => 1 + 1 / (↑n + 1)) > LIM b
⊢ (↑fun n => 1 + 1 / (↑n + 1)).IsCauchy ∧
(↑fun n => 1 - 1 / (↑n + 1)).IsCauchy ∧
(∀ (n : ℕ), 1 + 1 / (↑n + 1) > (fun n => 1 - 1 / (↑n + 1)) n) ∧
¬(LIM fun n => 1 + 1 / (↑n + 1)) > LIM fun n => 1 - 1 / (↑n + 1)
All goals completed! 🐙Твердження 5.4.12 (Обмеження дійсних чисел раціональними)
theorem Real.exists_rat_le_and_nat_gt {x:Real} (hx: x.IsPos) :
(∃ q:ℚ, q > 0 ∧ (q:Real) ≤ x) ∧ ∃ N:ℕ, x < (N:Real) := x:Realhx:x.IsPos⊢ (∃ q > 0, ↑q ≤ x) ∧ ∃ N, x < ↑N
-- Доведення написане так, щоб відповідати структурі оригінального тексту.
x:Realhx:∃ a, BoundedAwayPos a ∧ (↑a).IsCauchy ∧ x = LIM a⊢ (∃ q > 0, ↑q ≤ x) ∧ ∃ N, x < ↑N; x:Reala:ℕ → ℚhbound:BoundedAwayPos ahcauchy:(↑a).IsCauchyheq:x = LIM a⊢ (∃ q > 0, ↑q ≤ x) ∧ ∃ N, x < ↑N
x:Reala:ℕ → ℚhbound:∃ c > 0, ∀ (n : ℕ), a n ≥ chcauchy:(↑a).IsCauchyheq:x = LIM a⊢ (∃ q > 0, ↑q ≤ x) ∧ ∃ N, x < ↑N; x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ q⊢ (∃ q > 0, ↑q ≤ x) ∧ ∃ N, x < ↑N
x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qthis:?_mvar.836420 := Chapter5.Sequence.isBounded_of_isCauchy _fvar.836389⊢ (∃ q > 0, ↑q ≤ x) ∧ ∃ N, x < ↑N
x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qthis:∃ M ≥ 0, (↑a).BoundedBy M⊢ (∃ q > 0, ↑q ≤ x) ∧ ∃ N, x < ↑N; x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:(↑a).BoundedBy r⊢ (∃ q > 0, ↑q ≤ x) ∧ ∃ N, x < ↑N
x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ r⊢ (∃ q > 0, ↑q ≤ x) ∧ ∃ N, x < ↑N
x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ r⊢ ↑q ≤ xx:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ r⊢ ∃ N, x < ↑N
x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ r⊢ ↑q ≤ x x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ r⊢ ↑q = LIM fun x => q
All goals completed! 🐙
x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ rN:ℕhN:r < ↑N⊢ ∃ N, x < ↑N; x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ rN:ℕhN:r < ↑N⊢ x < ↑N
calc
x ≤ r := x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ rN:ℕhN:r < ↑N⊢ x ≤ ↑r
x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ rN:ℕhN:r < ↑N⊢ x ≤ LIM fun x => r
x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ rN:ℕhN:r < ↑N⊢ ∀ (n : ℕ), a n ≤ r
x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ rN:ℕhN:r < ↑Nn:ℕ⊢ a n ≤ r; x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0N:ℕhN:r < ↑Nn:ℕthis:|if 0 ≤ ↑n then a (↑n).toNat else 0| ≤ r⊢ a n ≤ r; x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0N:ℕhN:r < ↑Nn:ℕthis:|a n| ≤ r⊢ a n ≤ r
All goals completed! 🐙
_ < ((N:ℚ):Real) := x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyheq:x = LIM aq:ℚhq:q > 0hbound:∀ (n : ℕ), a n ≥ qr:ℚhr:r ≥ 0this:∀ (n : ℤ), |if 0 ≤ n then a n.toNat else 0| ≤ rN:ℕhN:r < ↑N⊢ ↑r < ↑↑N All goals completed! 🐙
_ = N := rflНаслідок 5.4.13 (Архімедова властивість )
theorem Real.le_mul {ε:Real} (hε: ε.IsPos) (x:Real) : ∃ M:ℕ, M > 0 ∧ M * ε > x := ε:Realhε:ε.IsPosx:Real⊢ ∃ M > 0, ↑M * ε > x
-- Доведення написане так, щоб відповідати структурі оригінального тексту.
ε:Realhε:ε.IsPos⊢ ∃ M > 0, ↑M * ε > 0ε:Realhε:ε.IsPosx:Realhx:x.IsPos⊢ ∃ M > 0, ↑M * ε > xε:Realhε:ε.IsPosx:Realhx:x.IsNeg⊢ ∃ M > 0, ↑M * ε > x
ε:Realhε:ε.IsPos⊢ ∃ M > 0, ↑M * ε > 0 ε:Realhε:ε.IsPos⊢ 1 > 0 ∧ ↑1 * ε > 0; All goals completed! 🐙
ε:Realhε:ε.IsPosx:Realhx:x.IsPos⊢ ∃ M > 0, ↑M * ε > x ε:Realhε:ε.IsPosx:Realhx:x.IsPosN:ℕhN:x / ε < ↑N⊢ ∃ M > 0, ↑M * ε > x
ε:Realhε:ε.IsPosx:Realhx:x.IsPosN:ℕhN:x / ε < ↑NM:ℕ := _fvar.851097 + 1⊢ ∃ M > 0, ↑M * ε > x; refine ⟨ M, ε:Realhε:ε.IsPosx:Realhx:x.IsPosN:ℕhN:x / ε < ↑NM:ℕ := _fvar.851097 + 1⊢ M > 0 All goals completed! 🐙, ?_ ⟩
replace hN : x/ε < M := hN.trans (ε:Realhε:ε.IsPosx:Realhx:x.IsPosN:ℕhN:x / ε < ↑NM:ℕ := _fvar.851097 + 1⊢ ↑N < ↑M All goals completed! 🐙)
ε:Realhε:ε.IsPosx:Realhx:x.IsPosN:ℕM:ℕ := _fvar.851097 + 1hN:_fvar.847941 / _fvar.847939 < ↑_fvar.851186 := LT.lt.trans _fvar.851100 ?_mvar.853499⊢ x < ↑M * ε
ε:Realhε:ε.IsPosx:Realhx:x.IsPosN:ℕM:ℕ := _fvar.851097 + 1hN:_fvar.847941 / _fvar.847939 < ↑_fvar.851186 := LT.lt.trans _fvar.851100 ?_mvar.853499⊢ x = x / ε * ε
ε:Realhε:ε > 0x:Realhx:x.IsPosN:ℕM:ℕ := _fvar.859018 + 1hN:x / ε < ↑M⊢ x = x / ε * ε; All goals completed! 🐙
ε:Realhε:ε.IsPosx:Realhx:x.IsNeg⊢ 1 > 0 ∧ ↑1 * ε > x; ε:Realx:Realhε:0 < εhx:x < 0⊢ x < ε; All goals completed! 🐙Твердження 5.4.14 / Вправа 5.4.5
theorem Real.rat_between {x y:Real} (hxy: x < y) : ∃ q:ℚ, x < (q:Real) ∧ (q:Real) < y := x:Realy:Realhxy:x < y⊢ ∃ q, x < ↑q ∧ ↑q < y All goals completed! 🐙Вправа 5.4.3
theorem Real.floor_exist (x:Real) : ∃! n:ℤ, (n:Real) ≤ x ∧ x < (n:Real)+1 := x:Real⊢ ∃! n, ↑n ≤ x ∧ x < ↑n + 1 All goals completed! 🐙Вправа 5.4.4
theorem Real.exist_inv_nat_le {x:Real} (hx: x.IsPos) : ∃ N:ℤ, N>0 ∧ (N:Real)⁻¹ < x := x:Realhx:x.IsPos⊢ ∃ N > 0, (↑N)⁻¹ < x All goals completed! 🐙Вправа 5.4.6
theorem Real.dist_lt_iff (ε x y:Real) : |x-y| < ε ↔ y-ε < x ∧ x < y+ε := ε:Realx:Realy:Real⊢ |x - y| < ε ↔ y - ε < x ∧ x < y + ε All goals completed! 🐙Вправа 5.4.6
theorem Real.dist_le_iff (ε x y:Real) : |x-y| ≤ ε ↔ y-ε ≤ x ∧ x ≤ y+ε := ε:Realx:Realy:Real⊢ |x - y| ≤ ε ↔ y - ε ≤ x ∧ x ≤ y + ε All goals completed! 🐙Вправа 5.4.7
theorem Real.le_add_eps_iff (x y:Real) : (∀ ε > 0, x ≤ y+ε) ↔ x ≤ y := x:Realy:Real⊢ (∀ ε > 0, x ≤ y + ε) ↔ x ≤ y All goals completed! 🐙Вправа 5.4.7
theorem Real.dist_le_eps_iff (x y:Real) : (∀ ε > 0, |x-y| ≤ ε) ↔ x = y := x:Realy:Real⊢ (∀ ε > 0, |x - y| ≤ ε) ↔ x = y All goals completed! 🐙Вправа 5.4.8
theorem Real.LIM_of_le {x:Real} {a:ℕ → ℚ} (hcauchy: (a:Sequence).IsCauchy) (h: ∀ n, a n ≤ x) :
LIM a ≤ x := x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyh:∀ (n : ℕ), ↑(a n) ≤ x⊢ LIM a ≤ x All goals completed! 🐙Вправа 5.4.8
theorem Real.LIM_of_ge {x:Real} {a:ℕ → ℚ} (hcauchy: (a:Sequence).IsCauchy) (h: ∀ n, a n ≥ x) :
LIM a ≥ x := x:Reala:ℕ → ℚhcauchy:(↑a).IsCauchyh:∀ (n : ℕ), ↑(a n) ≥ x⊢ LIM a ≥ x All goals completed! 🐙theorem Real.max_eq (x y:Real) : max x y = if x ≥ y then x else y := max_def' x ytheorem Real.min_eq (x y:Real) : min x y = if x ≤ y then x else y := rflВправа 5.4.9
theorem Real.neg_max (x y:Real) : max x y = - min (-x) (-y) := x:Realy:Real⊢ max x y = -min (-x) (-y) All goals completed! 🐙Вправа 5.4.9
theorem Real.neg_min (x y:Real) : min x y = - max (-x) (-y) := x:Realy:Real⊢ min x y = -max (-x) (-y) All goals completed! 🐙Вправа 5.4.9
theorem Real.max_comm (x y:Real) : max x y = max y x := x:Realy:Real⊢ max x y = max y x All goals completed! 🐙Вправа 5.4.9
theorem Real.max_self (x:Real) : max x x = x := x:Real⊢ max x x = x All goals completed! 🐙Вправа 5.4.9
theorem Real.max_add (x y z:Real) : max (x + z) (y + z) = max x y + z := x:Realy:Realz:Real⊢ max (x + z) (y + z) = max x y + z All goals completed! 🐙Вправа 5.4.9
theorem Real.max_mul (x y :Real) {z:Real} (hz: z.IsPos) : max (x * z) (y * z) = max x y * z := x:Realy:Realz:Realhz:z.IsPos⊢ max (x * z) (y * z) = max x y * z
All goals completed! 🐙/- Додаткова вправа: Що відбудеться, якщо z є від’ємним? -/Вправа 5.4.9
theorem Real.min_comm (x y:Real) : min x y = min y x := x:Realy:Real⊢ min x y = min y x All goals completed! 🐙Вправа 5.4.9
theorem Real.min_self (x:Real) : min x x = x := x:Real⊢ min x x = x All goals completed! 🐙Вправа 5.4.9
theorem Real.min_add (x y z:Real) : min (x + z) (y + z) = min x y + z := x:Realy:Realz:Real⊢ min (x + z) (y + z) = min x y + z All goals completed! 🐙Вправа 5.4.9
theorem Real.min_mul (x y :Real) {z:Real} (hz: z.IsPos) : min (x * z) (y * z) = min x y * z := x:Realy:Realz:Realhz:z.IsPos⊢ min (x * z) (y * z) = min x y * z
All goals completed! 🐙Вправа 5.4.9
theorem Real.inv_max {x y :Real} (hx:x.IsPos) (hy:y.IsPos) : (max x y)⁻¹ = min x⁻¹ y⁻¹ := x:Realy:Realhx:x.IsPoshy:y.IsPos⊢ (max x y)⁻¹ = min x⁻¹ y⁻¹ All goals completed! 🐙Вправа 5.4.9
theorem Real.inv_min {x y :Real} (hx:x.IsPos) (hy:y.IsPos) : (min x y)⁻¹ = max x⁻¹ y⁻¹ := x:Realy:Realhx:x.IsPoshy:y.IsPos⊢ (min x y)⁻¹ = max x⁻¹ y⁻¹ All goals completed! 🐙Не з підручника: раціональні числа вкладаються в дійсні як гомоморфізм впорядкованих кілець.
abbrev Real.ratCast_ordered_hom : ℚ →+*o Real where
toRingHom := ratCast_hom
monotone' := ⊢ Monotone (↑↑ratCast_hom).toFun All goals completed! 🐙end Chapter5