Documentation

Analysis.Section_2_3

Аналіз I, Глава 2.3 #

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

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

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

Визначення множення та піднесення до степеня для натуральних чисел з "Розділу 2". Chapter2.Nat

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

@[reducible, inline]

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

Визначення 2.3.1 (Множення натуральних чисел)

Equations

n.mul m = Chapter2.Nat.recurse (fun (x prod : Chapter2.Nat) => prod + m) 0 n

Instances For

instance Chapter2.Nat.instMul :

Equations

Chapter2.Nat.instMul = { mul := Chapter2.Nat.mul }

theorem Chapter2.Nat.zero_mul (m : Nat) :

0 * m = 0

Визначення 2.3.1 (Множення натуральних чисел)

theorem Chapter2.Nat.succ_mul (n m : Nat) :

n++ * m = n * m + m

Визначення 2.3.1 (Множення натуральних чисел)

theorem Chapter2.Nat.one_mul' (m : Nat) :

1 * m = 0 + m

theorem Chapter2.Nat.one_mul (m : Nat) :

1 * m = m

theorem Chapter2.Nat.two_mul (m : Nat) :

2 * m = 0 + m + m

theorem Chapter2.Nat.mul_zero (n : Nat) :

n * 0 = 0

Ця лема буде корисною для доведення Леми 2.3.2.

theorem Chapter2.Nat.mul_succ (n m : Nat) :

n * m++ = n * m + n

Ця лема буде корисною для доведення Леми 2.3.2.

theorem Chapter2.Nat.mul_comm (n m : Nat) :

n * m = m * n

Лема 2.3.2 (Множення комутативне) / Вправа 2.3.1

theorem Chapter2.Nat.mul_one (m : Nat) :

m * 1 = m

theorem Chapter2.Nat.mul_eq_zero_iff (n m : Nat) :

n * m = 0 ↔ n = 0 ∨ m = 0

Лема 2.3.3 (Додатні натуральні числа не мають дільників на нуль) / Вправа 2.3.2

theorem Chapter2.Nat.pos_mul_pos {n m : Nat} (h₁ : n.isPos) (h₂ : m.isPos) :

(n * m).isPos

theorem Chapter2.Nat.mul_add (a b c : Nat) :

a * (b + c) = a * b + a * c

Твердження 2.3.4 (Дістрібутивність)

theorem Chapter2.Nat.add_mul (a b c : Nat) :

(a + b) * c = a * c + b * c

Твердження 2.3.4 (Дістрібутивність)

theorem Chapter2.Nat.mul_assoc (a b c : Nat) :

a * b * c = a * (b * c)

Твердження 2.3.5 (Множення асоціативне) / Вправа 2.3.3

instance Chapter2.Nat.instCommSemiring :

CommSemiring Nat

(Не із книги) Nat є комутативним півкільцем.

Equations

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

theorem Chapter2.Nat.mul_lt_mul_of_pos_right {a b c : Nat} (h : a < b) (hc : c.isPos) :

a * c < b * c

Твердження 2.3.6 (Множення зберігає порядок)

theorem Chapter2.Nat.mul_gt_mul_of_pos_right {a b c : Nat} (h : a > b) (hc : c.isPos) :

a * c > b * c

Твердження 2.3.6 (Множення зберігає порядок)

theorem Chapter2.Nat.mul_lt_mul_of_pos_left {a b c : Nat} (h : a < b) (hc : c.isPos) :

c * a < c * b

Твердження 2.3.6 (Множення зберігає порядок)

theorem Chapter2.Nat.mul_gt_mul_of_pos_left {a b c : Nat} (h : a > b) (hc : c.isPos) :

c * a > c * b

Твердження 2.3.6 (Множення зберігає порядок)

theorem Chapter2.Nat.mul_cancel_right {a b c : Nat} (h : a * c = b * c) (hc : c.isPos) :

a = b

Наслідок 2.3.7 (Властивість скорочення)

instance Chapter2.Nat.isOrderedRing :

IsOrderedRing Nat

(Не із книги) Nat є впорядкованим півкільцем.

theorem Chapter2.Nat.exists_div_mod (n : Nat) {q : Nat} (hq : q.isPos) :

∃ (m : Nat) (r : Nat), 0 ≤ r ∧ r < q ∧ n = m * q + r

Твердження 2.3.9 (Лема про ділення Евкліда) / Вправа 2.3.5

@[reducible, inline]

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

Визначення 2.3.11 (Піднесення до степеня для натуральних чисел)

Equations

m.pow n = Chapter2.Nat.recurse (fun (x prod : Chapter2.Nat) => prod * m) 1 n

Instances For

instance Chapter2.Nat.instPow :

HomogeneousPow Nat

Equations

Chapter2.Nat.instPow = { pow := Chapter2.Nat.pow }

theorem Chapter2.Nat.pow_zero (m : Nat) :

m ^ 0 = 1

Визначення 2.3.11 (Піднесення до степеня для натуральних чисел)

theorem Chapter2.Nat.zero_pow_zero :

0 ^ 0 = 1

Визначення 2.3.11 (Піднесення до степеня для натуральних чисел)

theorem Chapter2.Nat.pow_succ (m n : Nat) :

m ^ n++ = m ^ n * m

Визначення 2.3.11 (Піднесення до степеня для натуральних чисел)

theorem Chapter2.Nat.sq_add_eq (a b : Nat) :

(a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2

Вправа 2.3.4