Аналіз I, Розділ 4.4: Прогалини у раціональних числах

Я (пр.перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним рішенням Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підбуцнути", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.

Основні побудови та результати цього розділу:

• Ірраціональність √2 та пов’язані факти про раціональні числа

Багато результатів тут можна встановити швидше, більше спираючись на API Mathlib; можна поставити собі вправу зробити це.

Підказки від попередніх користувачів

Користувачі супровідного матеріалу, які виконали вправи в цьому розділі, можуть надсилати свої поради майбутнім користувачам цього розділу як PRи.

• (Додайте підказку тут)

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

Твердження 4.4.1 (Переплетення цілих чисел раціональними) / Вправа 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 (Переплетення раціональних чисел)

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

Вправа 4.4.2 (a)

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

Вправа 4.4.2 (b)

Equations

• Int.infinite_descent = sorry

def Rat.pos_infinite_descent : Decidable (∃ (a : ℕ → { x : ℚ // 0 < x }), ∀ (n : ℕ), a (n + 1) < a n)

Вправа 4.4.2 (b)

Equations

• Rat.pos_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