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

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

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

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

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

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

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

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

namespace Section_4_1structure PreInt where minuend : ℕ subtrahend : ℕ @[simp] theorem PreInt.eq (a b c d:ℕ) : (⟨ a,b ⟩: PreInt) ≈ ⟨ c,d ⟩ ↔ a + d = c + b := bya:ℕb:ℕc:ℕd:ℕ⊢ { minuend := a, subtrahend := b } ≈ { minuend := c, subtrahend := d } ↔ a + d = c + b rflAll goals completed! 🐙abbrev Int := Quotient PreInt.instSetoidabbrev Int.formalDiff (a b:ℕ) : Int := Quotient.mk PreInt.instSetoid ⟨ a,b ⟩infix:100 " —— " => Int.formalDiff instance Int.instMul : Mul Int where mul := Quotient.lift₂ (fun ⟨ a, b ⟩ ⟨ c, d ⟩ ↦ (a * c + b * d) —— (a * d + b * c)) (by⊢ ∀ (a₁ b₁ a₂ b₂ : PreInt), a₁ ≈ a₂ → b₁ ≈ b₂ → (fun x x_1 => match x with | { minuend := a, subtrahend := b } => match x_1 with | { minuend := c, subtrahend := d } => (a * c + b * d) —— (a * d + b * c)) a₁ b₁ = (fun x x_1 => match x with | { minuend := a, subtrahend := b } => match x_1 with | { minuend := c, subtrahend := d } => (a * c + b * d) —— (a * d + b * c)) a₂ b₂ intro ⟨ a, b ⟩ ⟨ c, d ⟩ ⟨ a', b' ⟩ ⟨ c', d' ⟩ h1 h2a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:{ minuend := a, subtrahend := b } ≈ { minuend := a', subtrahend := b' }h2:{ minuend := c, subtrahend := d } ≈ { minuend := c', subtrahend := d' }⊢ (fun x x_1 => match x with | { minuend := a, subtrahend := b } => match x_1 with | { minuend := c, subtrahend := d } => (a * c + b * d) —— (a * d + b * c)) { minuend := a, subtrahend := b } { minuend := c, subtrahend := d } = (fun x x_1 => match x with | { minuend := a, subtrahend := b } => match x_1 with | { minuend := c, subtrahend := d } => (a * c + b * d) —— (a * d + b * c)) { minuend := a', subtrahend := b' } { minuend := c', subtrahend := d' } simp at h1 h2a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ (fun x x_1 => match x with | { minuend := a, subtrahend := b } => match x_1 with | { minuend := c, subtrahend := d } => (a * c + b * d) —— (a * d + b * c)) { minuend := a, subtrahend := b } { minuend := c, subtrahend := d } = (fun x x_1 => match x with | { minuend := a, subtrahend := b } => match x_1 with | { minuend := c, subtrahend := d } => (a * c + b * d) —— (a * d + b * c)) { minuend := a', subtrahend := b' } { minuend := c', subtrahend := d' } convert mul_congr _ _convert_9a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ a —— b = a' —— b'convert_10a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ c —— d = c' —— d' <;>convert_9a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ a —— b = a' —— b'convert_10a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ c —— d = c' —— d' simpaAll goals completed! 🐙 ) instance Int.instOfNat {n:ℕ} : OfNat Int n where ofNat := n —— 0instance Int.instNatCast : NatCast Int where natCast n := n —— 0theorem Int.ofNat_eq (n:ℕ) : ofNat(n) = n —— 0 := rfltheorem Int.natCast_eq (n:ℕ) : (n:Int) = n —— 0 := rfl@[simp] theorem Int.natCast_ofNat (n:ℕ) : ((ofNat(n):ℕ): Int) = ofNat(n) := byn:ℕ⊢ ↑(OfNat.ofNat n) = OfNat.ofNat n rflAll goals completed! 🐙@[simp] theorem Int.ofNat_inj (n m:ℕ) : (ofNat(n) : Int) = (ofNat(m) : Int) ↔ ofNat(n) = ofNat(m) := byn:ℕm:ℕ⊢ OfNat.ofNat n = OfNat.ofNat m ↔ OfNat.ofNat n = OfNat.ofNat m simp only [ofNat_eq, eq, add_zero]n:ℕm:ℕ⊢ n = m ↔ OfNat.ofNat n = OfNat.ofNat m rflAll goals completed! 🐙@[simp] theorem Int.natCast_inj (n m:ℕ) : (n : Int) = (m : Int) ↔ n = m := byn:ℕm:ℕ⊢ ↑n = ↑m ↔ n = m simp only [natCast_eq, eq, add_zero]All goals completed! 🐙example : 3 = 3 —— 0 := by⊢ 3 = 3 —— 0 rflAll goals completed! 🐙example : 3 = 4 —— 1 := by⊢ 3 = 4 —— 1 rw [Int.ofNat_eq, Int.eq]All goals completed! 🐙 theorem Int.neg_eq (a b:ℕ) : -(a —— b) = b —— a := rflexample : -(3 —— 5) = 5 —— 3 := by⊢ -3 —— 5 = 5 —— 3 rflAll goals completed! 🐙abbrev Int.isPos (x:Int) : Prop := ∃ (n:ℕ), n > 0 ∧ x = nabbrev Int.isNeg (x:Int) : Prop := ∃ (n:ℕ), n > 0 ∧ x = -n theorem declaration uses 'sorry'Int.sub_eq_formal_sub (a b:ℕ) : (a:Int) - (b:Int) = a —— b := bya:ℕb:ℕ⊢ ↑a - ↑b = a —— b sorryAll goals completed! 🐙 theorem Int.le_iff (a b:Int) : a ≤ b ↔ ∃ t:ℕ, b = a + t := bya:Intb:Int⊢ a ≤ b ↔ ∃ t, b = a + ↑t rflAll goals completed! 🐙theorem Int.lt_iff (a b:Int): a < b ↔ (∃ t:ℕ, b = a + t) ∧ a ≠ b := bya:Intb:Int⊢ a < b ↔ (∃ t, b = a + ↑t) ∧ a ≠ b rflAll goals completed! 🐙 end Section_4_1