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

Цей файл є перекладом Глави 2.2 Аналізу I до Lean 4. Вся нумерація посилається на оригінальний текст.

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

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

• Визначення додавання та порядку для натуральних чисел "Розділу 2", Chapter2.Nat
• Встановлення основних властивостей додавання та порядку

Примітка: наприкінці цього розділу клас Chapter2.Nat буде замінено на користь стандартного класу Mathlib _root_.Nat, або ℕ. Однак, ми пропрацюємо властивості Chapter2.Nat "вручну" в наступних кількох розділах для педагогічних цілей.

@[reducible, inline]

abbrev Chapter2.Nat.add (n m : Nat) : Nat

Визначення 2.2.1. (Додавання натуральних чисел. Порівняйте із Mathlib-овським Nat.add

Equations

• n.add m = Chapter2.Nat.recurse (fun (x sum : Chapter2.Nat) => sum++) m n

instance Chapter2.Nat.instAdd : Add Nat

Цей екземпляр дозволить нотації + використовуватися для додавання натуральних чисел.

Equations

• Chapter2.Nat.instAdd = { add := Chapter2.Nat.add }

@[simp]

theorem Chapter2.Nat.zero_add (m : Nat) : 0 + m = m

Порівняйте із Mathlib-овським Nat.zero_add

theorem Chapter2.Nat.succ_add (n m : Nat) : n++ + m = (n + m)++

Порівняйте із Mathlib-овським Nat.succ_add

theorem Chapter2.Nat.one_add (m : Nat) : 1 + m = m++

Порівняйте із Mathlib-овським Nat.one_add

theorem Chapter2.Nat.two_add (m : Nat) : 2 + m = m++++

@[simp]

theorem Chapter2.Nat.add_zero (n : Nat) : n + 0 = n

Лема 2.2.2 (n + 0 = n). Порівняйте із Mathlib-овським Nat.add_zero

theorem Chapter2.Nat.add_succ (n m : Nat) : n + m++ = (n + m)++

Лема 2.2.3 (n+(m++) = (n+m)++). Порівняйте із Mathlib-овським Nat.add_succ

theorem Chapter2.Nat.succ_eq_add_one (n : Nat) : n++ = n + 1

n++ = n + 1 (Чому?). Порівняйте із Mathlib-овським Nat.succ_eq_add_one

theorem Chapter2.Nat.add_comm (n m : Nat) : n + m = m + n

Твердження 2.2.4 (Додавання комутативне). Порівняйте із Mathlib-овським Nat.add_comm

theorem Chapter2.Nat.add_assoc (a b c : Nat) : a + b + c = a + (b + c)

Твердження 2.2.5 (Додавання асоціативне) / Вправа 2.2.1 Порівняйте із Mathlib-овським Nat.add_assoc

theorem Chapter2.Nat.add_left_cancel (a b c : Nat) (habc : a + b = a + c) : b = c

Твердження 2.2.6 (Властивість скорочення) Порівняйте із Mathlib-овським Nat.add_left_cancel

instance Chapter2.Nat.addCommMonoid : AddCommMonoid Nat

(Не із книги) Типу Nat можна дати структуру комутативного адітивного моноїда.

Equations

• One or more equations did not get rendered due to their size.

def Chapter2.Nat.isPos (n : Nat) : Prop

Визначення 2.2.7 (Додатні натуральні числе).

Equations

• n.isPos = (n ≠ 0)

theorem Chapter2.Nat.isPos_iff (n : Nat) : n.isPos ↔ n ≠ 0

theorem Chapter2.Nat.add_pos_left {a : Nat} (b : Nat) (ha : a.isPos) : (a + b).isPos

Твердження 2.2.8 (Додатне плюс натуральне число буде додатним). Порівняйте із Mathlib-овським Nat.add_pos_left

theorem Chapter2.Nat.add_pos_right {a : Nat} (b : Nat) (ha : a.isPos) : (b + a).isPos

Порівняйте із Mathlib-овським Nat.add_pos_right

theorem Chapter2.Nat.add_eq_zero (a b : Nat) (hab : a + b = 0) : a = 0 ∧ b = 0

Наслідок 2.2.9 (якщо сума дорівнює нулю, тоді доданки дорівнюють нулю). Порівняйте із Mathlib-овським Nat.add_eq_zero

theorem Chapter2.Nat.uniq_succ_eq (a : Nat) (ha : a.isPos) : ∃! b : Nat, b++ = a

Лема 2.2.10 (унікальний попередник) / Вправа 2.2.2

instance Chapter2.Nat.instLE : LE Nat

Визначення 2.2.11 (Порядок натуральних чисел) Це визначає операцію ≤ на натуральних числах.

Equations

• Chapter2.Nat.instLE = { le := fun (n m : Chapter2.Nat) => ∃ (a : Chapter2.Nat), m = n + a }

instance Chapter2.Nat.instLT : LT Nat

Визначення 2.2.11 (Порядок натуральних чисел) Це визначає операцію < на натуральних числах.

Equations

• Chapter2.Nat.instLT = { lt := fun (n m : Chapter2.Nat) => n ≤ m ∧ n ≠ m }

theorem Chapter2.Nat.le_iff (n m : Nat) : n ≤ m ↔ ∃ (a : Nat), m = n + a

theorem Chapter2.Nat.lt_iff (n m : Nat) : n < m ↔ (∃ (a : Nat), m = n + a) ∧ n ≠ m

theorem Chapter2.Nat.ge_iff_le (n m : Nat) : n ≥ m ↔ m ≤ n

Порівняйте із Mathlib-овським ge_iff_le

theorem Chapter2.Nat.gt_iff_lt (n m : Nat) : n > m ↔ m < n

Порівняйте із Mathlib-овським gt_iff_lt

theorem Chapter2.Nat.le_of_lt {n m : Nat} (hnm : n < m) : n ≤ m

Порівняйте із Mathlib-овським Nat.le_of_lt

theorem Chapter2.Nat.le_iff_lt_or_eq (n m : Nat) : n ≤ m ↔ n < m ∨ n = m

Порівняйте із Mathlib-овським Nat.le_iff_lt_or_eq

theorem Chapter2.Nat.succ_gt_self (n : Nat) : n++ > n

Порівняйте із Mathlib-овським Nat.lt_succ_self

theorem Chapter2.Nat.ge_refl (a : Nat) : a ≥ a

Твердження 2.2.12 (Базові властивості порядку для натуральних чисел) / Вправа 2.2.3

(a) (Порядок рефлексівен). Порівняйте із Mathlib-овським Nat.le_refl

theorem Chapter2.Nat.ge_trans {a b c : Nat} (hab : a ≥ b) (hbc : b ≥ c) : a ≥ c

(b) (Порядок транзітивен). Тут буде корисною тактика obtain. Порівняйте із Mathlib-овським Nat.le_trans

theorem Chapter2.Nat.ge_antisymm {a b : Nat} (hab : a ≥ b) (hba : b ≥ a) : a = b

(c) (Порядок антисіметричен). Порівняйте із Mathlib-овським Nat.le_antisymm

theorem Chapter2.Nat.add_ge_add_right (a b c : Nat) : a ≥ b ↔ a + c ≥ b + c

(d) (Додавання зберігає порядок). Порівняйте із Mathlib-овським Nat.add_le_add_right

theorem Chapter2.Nat.add_ge_add_left (a b c : Nat) : a ≥ b ↔ c + a ≥ c + b

(d) (Додавання зберігає порядок). Порівняйте із Mathlib-овським Nat.add_le_add_left

theorem Chapter2.Nat.add_le_add_right (a b c : Nat) : a ≤ b ↔ a + c ≤ b + c

(d) (Додавання зберігає порядок). Порівняйте із Mathlib-овським Nat.add_le_add_right

theorem Chapter2.Nat.add_le_add_left (a b c : Nat) : a ≤ b ↔ c + a ≤ c + b

(d) (Додавання зберігає порядок). Порівняйте із Mathlib-овським Nat.add_le_add_left

theorem Chapter2.Nat.lt_iff_succ_le (a b : Nat) : a < b ↔ a++ ≤ b

(e) a < b iff a++ ≤ b. Порівняйте із Mathlib-овським Nat.succ_le_iff

theorem Chapter2.Nat.lt_iff_add_pos (a b : Nat) : a < b ↔ ∃ (d : Nat), d.isPos ∧ b = a + d

(f) a < b if and only if b = a + d for positive d.

theorem Chapter2.Nat.ne_of_lt (a b : Nat) : a < b → a ≠ b

Якщо a < b тоді a ̸= b,

theorem Chapter2.Nat.ne_of_gt (a b : Nat) : a > b → a ≠ b

Якщо a > b тоді a ̸= b.

theorem Chapter2.Nat.not_lt_of_gt (a b : Nat) : a < b ∧ a > b → False

Якщо a > b та a < b тоді протиріччя

theorem Chapter2.Nat.trichotomous (a b : Nat) : a < b ∨ a = b ∨ a > b

Твердження 2.2.13 (Тріхотомія порядку для натуральних чисел) / Вправа 2.2.4 Порівняйте із Mathlib-овським trichotomous

def Chapter2.Nat.decLe (a b : Nat) : Decidable (a ≤ b)

(Не із книги) Встановіть алгоритмічну розв'язність для цього порядку обчислювальним шляхом. Частина доказу, що стосується розв'язності, наведена; решта sorry стосуються тверджень про натуральні числа. Цей результат також можна було б встановити за допомогою тактики classical з подальшим використанням exact Classical.decRel _, але це зробило б це визначення (а також деякі приклади нижче) необчислювальним.

Порівняйте із Mathlib-овським Nat.decLe

Equations

• One or more equations did not get rendered due to their size.
• Chapter2.Nat.zero.decLe x✝ = isTrue ⋯

instance Chapter2.Nat.decidableRel : DecidableRel fun (x1 x2 : Nat) => x1 ≤ x2

Equations

• Chapter2.Nat.decidableRel = Chapter2.Nat.decLe

instance Chapter2.Nat.linearOrder : LinearOrder Nat

(Не із книги) Nat має структуру лінійне впорядкування.

Equations

• One or more equations did not get rendered due to their size.

instance Chapter2.Nat.isOrderedAddMonoid : IsOrderedAddMonoid Nat

(Не із книги) Nat має структуру впорядкованого моноїда.

theorem Chapter2.Nat.strong_induction {m₀ : Nat} {P : Nat → Prop} (hind : ∀ m ≥ m₀, (∀ (m' : Nat), m₀ ≤ m' ∧ m' < m → P m') → P m) (m : Nat) : m ≥ m₀ → P m

Твердження 2.2.14 (Сильний принцип індукції) / Вправа 2.2.5 Порівняйте із Mathlib-овським Nat.strong_induction_on

theorem Chapter2.Nat.backwards_induction {n : Nat} {P : Nat → Prop} (hind : ∀ (m : Nat), P (m++) → P m) (hn : P n) (m : Nat) : m ≤ n → P m

Вправа 2.2.6 (індукція у зворотньому напрямку) Порівняйте із Mathlib-овським Nat.decreasingInduction

theorem Chapter2.Nat.induction_from {n : Nat} {P : Nat → Prop} (hind : ∀ (m : Nat), P m → P (m++)) : P n → ∀ m ≥ n, P m

Вправа 2.2.7 (індукція із початкової точки) Порівняйте із Mathlib-овським Nat.le_induction