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

У цій главі ми пропонуємо версію теорії множин Цермело-Франкеля (з атомами), яка намагається максимально точно наслідувати оригінальний тексту Аналізу I, Глава 4.1. Вся нумерація посилається на оригінальний текст.

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

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

• Definition of the "Section 4.1" integers, Section_4_1.Int, as formal differences a —— b of natural numbers a b:ℕ, up to equivalence. (This is a quotient of a scaffolding type Section_4_1.PreInt, which consists of formal differences without any equivalence imposed.)

• Визначення цілих чисел із "Глави 4.1", Section_4_1.Int, як формальна різниця a —— b натуральних чисел a b:ℕ, з точністю до еквівалентності. (Це частка типу каркасного типу Section_4_1.PreInt, яка складається з формальної різниці без будь-якої визначеної еквівалентності.)

• операції кільця та порядок цих цілих чисел, а також вкладення ℕ

• Еквівалентність із Mathlib-овськими цілими _root_.Int (або ℤ), які ми будемо використовувати в подальшому.

structure Section_4_1.PreInt : Type

• minuend : ℕ
• subtrahend : ℕ

instance Section_4_1.PreInt.instSetoid : Setoid PreInt

Визначення 4.1.1

Equations

• Section_4_1.PreInt.instSetoid = { r := fun (a b : Section_4_1.PreInt) => a.minuend + b.subtrahend = b.minuend + a.subtrahend, iseqv := Section_4_1.PreInt.instSetoid._proof_1 }

@[simp]

theorem Section_4_1.PreInt.eq (a b c d : ℕ) : { minuend := a, subtrahend := b } ≈ { minuend := c, subtrahend := d } ↔ a + d = c + b

@[reducible, inline]

abbrev Section_4_1.Int : Type

Equations

• Section_4_1.Int = Quotient Section_4_1.PreInt.instSetoid

@[reducible, inline]

abbrev Section_4_1.Int.formalDiff (a b : ℕ) : Int

Equations

• a —— b = ⟦{ minuend := a, subtrahend := b }⟧

def Section_4_1.«term_——_» : Lean.TrailingParserDescr

Equations

• Section_4_1.«term_——_» = Lean.ParserDescr.trailingNode `Section_4_1.«term_——_» 100 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " —— ") (Lean.ParserDescr.cat `term 101))

theorem Section_4_1.Int.eq (a b c d : ℕ) : a —— b = c —— d ↔ a + d = c + b

Визначення 4.1.1 (Цілі числа)

instance Section_4_1.Int.decidableEq : DecidableEq Int

Алгоритмічна розв'язність рівності

Equations

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

theorem Section_4_1.Int.eq_diff (n : Int) : ∃ (a : ℕ) (b : ℕ), n = a —— b

Визначення 4.1.1 (Integers)

instance Section_4_1.Int.instAdd : Add Int

Лема 4.1.3 (Додавання чітко визначене)

Equations

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

theorem Section_4_1.Int.add_eq (a b c d : ℕ) : a —— b + c —— d = (a + c) —— (b + d)

Визначення 4.1.2 (Визначення додавання)

theorem Section_4_1.Int.mul_congr_left (a b a' b' c d : ℕ) (h : a —— b = a' —— b') : (a * c + b * d) —— (a * d + b * c) = (a' * c + b' * d) —— (a' * d + b' * c)

Лема 4.1.3 (Множення чітко визначене)

theorem Section_4_1.Int.mul_congr_right (a b c d c' d' : ℕ) (h : c —— d = c' —— d') : (a * c + b * d) —— (a * d + b * c) = (a * c' + b * d') —— (a * d' + b * c')

Лема 4.1.3 (Множення чітко визначене)

theorem Section_4_1.Int.mul_congr {a b c d a' b' c' d' : ℕ} (h1 : a —— b = a' —— b') (h2 : c —— d = c' —— d') : (a * c + b * d) —— (a * d + b * c) = (a' * c' + b' * d') —— (a' * d' + b' * c')

Лема 4.1.3 (Множення чітко визначене)

instance Section_4_1.Int.instMul : Mul Int

Equations

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

theorem Section_4_1.Int.mul_eq (a b c d : ℕ) : a —— b * c —— d = (a * c + b * d) —— (a * d + b * c)

Визначення 4.1.2 (Множення цілих чисел)

instance Section_4_1.Int.instOfNat {n : ℕ} : OfNat Int n

Equations

• Section_4_1.Int.instOfNat = { ofNat := n —— 0 }

instance Section_4_1.Int.instNatCast : NatCast Int

Equations

• Section_4_1.Int.instNatCast = { natCast := fun (n : ℕ) => n —— 0 }

theorem Section_4_1.Int.ofNat_eq (n : ℕ) : OfNat.ofNat n = n —— 0

theorem Section_4_1.Int.natCast_eq (n : ℕ) : ↑n = n —— 0

@[simp]

theorem Section_4_1.Int.natCast_ofNat (n : ℕ) : ↑(OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem Section_4_1.Int.ofNat_inj (n m : ℕ) : OfNat.ofNat n = OfNat.ofNat m ↔ OfNat.ofNat n = OfNat.ofNat m

@[simp]

theorem Section_4_1.Int.natCast_inj (n m : ℕ) : ↑n = ↑m ↔ n = m

theorem Section_4_1.Int.cast_eq_0_iff_eq_0 (n : ℕ) : ↑n = 0 ↔ n = 0

(Не із книги) 0 is the only natural whose cast is 0

instance Section_4_1.Int.instNeg : Neg Int

Визначення 4.1.4 (Протилежність цілих чисел) / Вправа 4.1.2

Equations

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

theorem Section_4_1.Int.neg_eq (a b : ℕ) : -a —— b = b —— a

@[reducible, inline]

abbrev Section_4_1.Int.isPos (x : Int) : Prop

Equations

• x.isPos = ∃ n > 0, x = ↑n

@[reducible, inline]

abbrev Section_4_1.Int.isNeg (x : Int) : Prop

Equations

• x.isNeg = ∃ n > 0, x = -↑n

theorem Section_4_1.Int.trichotomous (x : Int) : x = 0 ∨ x.isPos ∨ x.isNeg

Лема 4.1.5 (трихотомія цілих чисел)

theorem Section_4_1.Int.not_pos_zero (x : Int) : x = 0 ∧ x.isPos → False

Лема 4.1.5 (трихотомія цілих чисел)

theorem Section_4_1.Int.not_neg_zero (x : Int) : x = 0 ∧ x.isNeg → False

Лема 4.1.5 (трихотомія цілих чисел)

theorem Section_4_1.Int.not_pos_neg (x : Int) : x.isPos ∧ x.isNeg → False

Лема 4.1.5 (трихотомія цілих чисел)

instance Section_4_1.Int.instAddGroup : AddGroup Int

Твердження 4.1.6 (закони алгебри) / Вправа 4.1.4

Equations

• Section_4_1.Int.instAddGroup = AddGroup.ofLeftAxioms Section_4_1.Int.instAddGroup._proof_10 Section_4_1.Int.instAddGroup._proof_11 Section_4_1.Int.instAddGroup._proof_12

instance Section_4_1.Int.instAddCommGroup : AddCommGroup Int

Твердження 4.1.6 (закони алгебри) / Вправа 4.1.4

Equations

• Section_4_1.Int.instAddCommGroup = { toAddGroup := Section_4_1.Int.instAddGroup, add_comm := Section_4_1.Int.instAddCommGroup._proof_13 }

instance Section_4_1.Int.instCommMonoid : CommMonoid Int

Твердження 4.1.6 (закони алгебри) / Вправа 4.1.4

Equations

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

instance Section_4_1.Int.instCommRing : CommRing Int

Твердження 4.1.6 (закони алгебри) / Вправа 4.1.4

Equations

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

theorem Section_4_1.Int.sub_eq (a b : Int) : a - b = a + -b

Визначення віднімання

theorem Section_4_1.Int.sub_eq_formal_sub (a b : ℕ) : ↑a - ↑b = a —— b

theorem Section_4_1.Int.mul_eq_zero {a b : Int} (h : a * b = 0) : a = 0 ∨ b = 0

Твердження 4.1.8 (Немає дільників нуля) / Вправа 4.1.5

theorem Section_4_1.Int.mul_right_cancel₀ (a b c : Int) (h : a * c = b * c) (hc : c ≠ 0) : a = b

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

instance Section_4_1.Int.instLE : LE Int

Визначення 4.1.10 (Упорядкування цілих чисел)

Equations

• Section_4_1.Int.instLE = { le := fun (n m : Section_4_1.Int) => ∃ (a : ℕ), m = n + ↑a }

instance Section_4_1.Int.instLT : LT Int

Визначення 4.1.10 (Упорядкування цілих чисел)

Equations

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

theorem Section_4_1.Int.le_iff (a b : Int) : a ≤ b ↔ ∃ (t : ℕ), b = a + ↑t

theorem Section_4_1.Int.lt_iff (a b : Int) : a < b ↔ (∃ (t : ℕ), b = a + ↑t) ∧ a ≠ b

theorem Section_4_1.Int.lt_iff_exists_positive_difference (a b : Int) : a < b ↔ ∃ (n : ℕ), n ≠ 0 ∧ b = a + ↑n

Лема 4.1.11(a) (Властивості упорядкування) / Вправа 4.1.7

theorem Section_4_1.Int.add_lt_add_right {a b : Int} (c : Int) (h : a < b) : a + c < b + c

Лема 4.1.11(b) (Додавання зберігає порядок) / Вправа 4.1.7

theorem Section_4_1.Int.mul_lt_mul_of_pos_right {a b c : Int} (hab : a < b) (hc : 0 < c) : a * c < b * c

Лема 4.1.11(c) (Додатне множення зберігає порядок) / Вправа 4.1.7

theorem Section_4_1.Int.neg_gt_neg {a b : Int} (h : b < a) : -a < -b

Лема 4.1.11(d) (Протилежність змінює порядок) / Вправа 4.1.7

theorem Section_4_1.Int.neg_ge_neg {a b : Int} (h : b ≤ a) : -a ≤ -b

Лема 4.1.11(d) (Протилежність змінює порядок) / Вправа 4.1.7

theorem Section_4_1.Int.lt_trans {a b c : Int} (hab : a < b) (hbc : b < c) : a < c

Лема 4.1.11(e) (Порядок транзитивний) / Вправа 4.1.7

theorem Section_4_1.Int.trichotomous' (a b : Int) : a > b ∨ a < b ∨ a = b

Лема 4.1.11(f) (Тріхотомія порядку) / Вправа 4.1.7

theorem Section_4_1.Int.not_gt_and_lt (a b : Int) : ¬(a > b ∧ a < b)

Лема 4.1.11(f) (Тріхотомія порядку) / Вправа 4.1.7

theorem Section_4_1.Int.not_gt_and_eq (a b : Int) : ¬(a > b ∧ a = b)

Лема 4.1.11(f) (Тріхотомія порядку) / Вправа 4.1.7

theorem Section_4_1.Int.not_lt_and_eq (a b : Int) : ¬(a < b ∧ a = b)

Лема 4.1.11(f) (Тріхотомія порядку) / Вправа 4.1.7

instance Section_4_1.Int.decidableRel : DecidableRel fun (x1 x2 : Int) => x1 ≤ x2

(Не із книги) Встановимо алгорітмічну розв'язність цього порядку.

Equations

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

theorem Section_4_1.Int.is_additive_identity_iff_eq_0 (b : Int) : (∀ (a : Int), a = a + b) ↔ b = 0

(Не із книги) 0 єдиний нейтральний елемент додавання

instance Section_4_1.Int.instLinearOrder : LinearOrder Int

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

Equations

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

theorem Section_4_1.Int.neg_one_mul (a : Int) : -1 * a = -a

Вправа 4.1.3

theorem Section_4_1.Int.no_induction : ∃ (P : Int → Prop), P 0 ∧ ∀ (n : Int), P n → P (n + 1) ∧ ¬∀ (n : Int), P n

Вправа 4.1.8

theorem Section_4_1.Int.sq_nonneg_of_pos (n : Int) (h : 0 ≤ n) : 0 ≤ n * n

Невід'ємне число в квадраті є невід'ємним. Це окремий випадок із 4.1.9, корисний для доведення загального випадку. -

theorem Section_4_1.Int.sq_nonneg (n : Int) : 0 ≤ n * n

Вправа 4.1.9. Квадрат будь-якого цілого числа є невід'ємним.

theorem Section_4_1.Int.sq_nonneg' (n : Int) : ∃ (m : ℕ), n * n = ↑m

Вправа 4.1.9

@[reducible, inline]

abbrev Section_4_1.Int.equivInt : Int ≃ ℤ

Не в книзі: створити еквівалентність між Int та ℤ. Це потребує деякої обізнанності із API Mathlib-овської версії цілих чисел.

Equations

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

@[reducible, inline]

abbrev Section_4_1.Int.equivInt_ordered_ring : Int ≃+*o ℤ

Не в книзі: еквівалентність зберігає порядок та операції з кільцем

Equations

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