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

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:

Ordering on the real line

namespace Chapter5

Визначення 5.4.1 (sequences bounded away from zero with sign). Sequences are indexed to start from zero as this is more convenient for Mathlib purposes.

abbrev bounded_away_pos (a:ℕ → ℚ) : Prop :=
  ∃ (c:ℚ), c > 0 ∧ ∀ n, a n ≥ c

Визначення 5.4.1 (sequences bounded away from zero with sign).

abbrev bounded_away_neg (a:ℕ → ℚ) : Prop :=
  ∃ (c:ℚ), c > 0 ∧ ∀ n, a n ≤ -c

Визначення 5.4.1 (sequences bounded away from zero with sign).

theorem bounded_away_pos_def (a:ℕ → ℚ) : bounded_away_pos a ↔ ∃ (c:ℚ), c > 0 ∧ ∀ n, a n ≥ c := bya:ℕ → ℚ⊢ bounded_away_pos a ↔ ∃ c > 0, ∀ (n : ℕ), a n ≥ c
  rflAll goals completed! 🐙

Визначення 5.4.1 (sequences bounded away from zero with sign).

theorem bounded_away_neg_def (a:ℕ → ℚ) : bounded_away_neg a ↔ ∃ (c:ℚ), c > 0 ∧ ∀ n, a n ≤ -c := bya:ℕ → ℚ⊢ bounded_away_neg a ↔ ∃ c > 0, ∀ (n : ℕ), a n ≤ -c
  rflAll goals completed! 🐙

Приклади 5.4.2

declaration uses 'sorry'example : bounded_away_pos (fun n ↦ 1 + 10^(-(n:ℤ)-1)) := by⊢ bounded_away_pos fun n => 1 + 10 ^ (-↑n - 1) sorryAll goals completed! 🐙

Приклади 5.4.2

declaration uses 'sorry'example : bounded_away_neg (fun n ↦ - - 10^(-(n:ℤ)-1)) := by⊢ bounded_away_neg fun n => - -10 ^ (-↑n - 1) sorryAll goals completed! 🐙

Приклади 5.4.2

declaration uses 'sorry'example : ¬ bounded_away_pos (fun n ↦ (-1)^n) := by⊢ ¬bounded_away_pos fun n => (-1) ^ n sorryAll goals completed! 🐙

declaration uses 'sorry'example : ¬ bounded_away_neg (fun n ↦ (-1)^n) := by⊢ ¬bounded_away_neg fun n => (-1) ^ n sorryAll goals completed! 🐙

declaration uses 'sorry'example : bounded_away_zero (fun n ↦ (-1)^n) := by⊢ bounded_away_zero fun n => (-1) ^ n sorryAll goals completed! 🐙

theorem declaration uses 'sorry'bounded_away_zero_of_pos {a:ℕ → ℚ} (ha: bounded_away_pos a) : bounded_away_zero a := bya:ℕ → ℚha:bounded_away_pos a⊢ bounded_away_zero a
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'bounded_away_zero_of_neg {a:ℕ → ℚ} (ha: bounded_away_neg a) : bounded_away_zero a := bya:ℕ → ℚha:bounded_away_neg a⊢ bounded_away_zero a
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'not_bounded_away_pos_neg {a:ℕ → ℚ} : ¬ (bounded_away_pos a ∧ bounded_away_neg a) := bya:ℕ → ℚ⊢ ¬(bounded_away_pos a ∧ bounded_away_neg a)
  sorryAll goals completed! 🐙

abbrev Real.isPos (x:Real) : Prop :=
  ∃ a:ℕ → ℚ, bounded_away_pos a ∧ (a:Sequence).isCauchy ∧ x = LIM a

abbrev Real.isNeg (x:Real) : Prop :=
  ∃ a:ℕ → ℚ, bounded_away_neg a ∧ (a:Sequence).isCauchy ∧ x = LIM a

theorem Real.isPos_def (x:Real) :
    Real.isPos x ↔ ∃ a:ℕ → ℚ, bounded_away_pos a ∧ (a:Sequence).isCauchy ∧ x = LIM a := byx:Real⊢ x.isPos ↔
  ∃ a,
    bounded_away_pos a ∧ { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ∧ x = LIM a rflAll goals completed! 🐙

theorem Real.isNeg_def (x:Real) :
    Real.isNeg x ↔ ∃ a:ℕ → ℚ, bounded_away_neg a ∧ (a:Sequence).isCauchy ∧ x = LIM a := byx:Real⊢ x.isNeg ↔
  ∃ a,
    bounded_away_neg a ∧ { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ∧ x = LIM a rflAll goals completed! 🐙