Аналіз I, Глава 4.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:

• Irrationality of √2, and related facts about the rational numbers

Many of the results here can be established more quickly by relying more heavily on the Mathlib API; one can set oneself the exercise of doing so.

theorem Rat.between_int (x : ℚ) : ∃! n : ℤ, ↑n ≤ x ∧ x < ↑n + 1

Твердження 4.4.1 (Interspersing of integers by rationals) / Вправа 4.4.1

theorem Nat.exists_gt (x : ℚ) : ∃ (n : ℕ), ↑n > x

theorem Rat.exists_between_rat {x y : ℚ} (h : x < y) : ∃ (z : ℚ), x < z ∧ z < y

Твердження 4.4.3 (Interspersing of rationals)

theorem Nat.no_infinite_descent : ¬∃ (a : ℕ → ℕ), ∀ (n : ℕ), a (n + 1) < a n

Вправа 4.4.2

def Int.infinite_descent : Decidable (∃ (a : ℕ → ℤ), ∀ (n : ℕ), a (n + 1) < a n)

Equations

• Int.infinite_descent = sorry

theorem Nat.even_or_odd'' (n : ℕ) : Even n ∨ Odd n

theorem Nat.not_even_and_odd (n : ℕ) : ¬(Even n ∧ Odd n)

theorem Rat.not_exist_sqrt_two : ¬∃ (x : ℚ), x ^ 2 = 2

Твердження 4.4.4 / Вправа 4.4.3

theorem Rat.exist_approx_sqrt_two {ε : ℚ} (hε : ε > 0) : ∃ x ≥ 0, x ^ 2 < 2 ∧ 2 < (x + ε) ^ 2

Твердження 4.4.5