The rationals

Аналіз I, Розділ 4.2: Раціональні числа

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

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

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

Визначення раціональних чисел «Розділу 4.2» Section_4_2.Rat : TypeSection_4_2.Rat як формальних часток Unknown identifier `a`sorry // sorry : Section_4_2.Rata // Unknown identifier `b`b цілих чисел , з точністю до еквівалентності. (Це фактортип допоміжного типу Section_4_2.PreRat : TypeSection_4_2.PreRat, який складається з формальних часток без накладеної еквівалентності.)
Операції поля та порядок на цих раціональних числах, а також вкладення ℕ і ℤ.
Еквівалентність із раціональними числами Mathlib Rat : Type_root_.Rat (або ℚ : Typeℚ), які ми надалі використовуватимемо.

Примітка: тут (і надалі) ми використовуємо натуральні числа ℕ : Typeℕ та цілі числа ℤ : Typeℤ із Mathlib, а не натуральні числа розділу 2 та цілі числа розділу 4.1.

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

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

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

namespace Section_4_2

structure PreRat where
  numerator : ℤ
  denominator : ℤ
  nonzero : denominator ≠ 0

Вправа 4.2.1

instance declaration uses 'sorry'PreRat.instSetoid : Setoid PreRat where
  r a b := a.numerator * b.denominator = b.numerator * a.denominator
  iseqv := {
    refl := by⊢ ∀ (x : PreRat), x.numerator * x.denominator = x.numerator * x.denominator sorryAll goals completed! 🐙
    symm := by⊢ ∀ {x y : PreRat},
  x.numerator * y.denominator = y.numerator * x.denominator → y.numerator * x.denominator = x.numerator * y.denominator sorryAll goals completed! 🐙
    trans := by⊢ ∀ {x y z : PreRat},
  x.numerator * y.denominator = y.numerator * x.denominator →
    y.numerator * z.denominator = z.numerator * y.denominator →
      x.numerator * z.denominator = z.numerator * x.denominator sorryAll goals completed! 🐙
    }

@[simp]
theorem PreRat.eq (a b c d:ℤ) (hb: b ≠ 0) (hd: d ≠ 0) :
    (⟨ a,b,hb ⟩: PreRat) ≈ ⟨ c,d,hd ⟩ ↔ a * d = c * b := bya:ℤb:ℤc:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ { numerator := a, denominator := b, nonzero := hb } ≈ { numerator := c, denominator := d, nonzero := hd } ↔
  a * d = c * b rflAll goals completed! 🐙

abbrev Rat := Quotient PreRat.instSetoid

Ми надаємо діленню «сміттєве» значення 0//1, якщо знаменник дорівнює нулю

abbrev Rat.formalDiv (a b:ℤ) : Rat :=
  Quotient.mk PreRat.instSetoid (if h:b ≠ 0 then ⟨ a,b,h ⟩ else ⟨ 0, 1, bya:ℤb:ℤh:¬b ≠ 0⊢ 1 ≠ 0 decideAll goals completed! 🐙 ⟩)

infix:100 " // " => Rat.formalDiv

Визначення 4.2.1 (Раціональні числа)

theorem Rat.eq (a c:ℤ) {b d:ℤ} (hb: b ≠ 0) (hd: d ≠ 0): a // b = c // d ↔ a * d = c * b := bya:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ a // b = c // d ↔ a * d = c * b
  simp [hb, hd, Setoid.r]All goals completed! 🐙

Визначення 4.2.1 (Раціональні числа)

theorem Rat.eq_diff (n:Rat) : ∃ a b, b ≠ 0 ∧ n = a // b := byn:Rat⊢ ∃ a b, b ≠ 0 ∧ n = a // b
  apply Quotient.ind _ nn:Rat⊢ ∀ (a : PreRat), ∃ a_1 b, b ≠ 0 ∧ ⟦a⟧ = a_1 // b; intro ⟨ a, b, h ⟩n:Rata:ℤb:ℤh:b ≠ 0⊢ ∃ a_1 b_1, b_1 ≠ 0 ∧ ⟦{ numerator := a, denominator := b, nonzero := h }⟧ = a_1 // b_1
  refine ⟨ a, b, h, ?_ ⟩n:Rata:ℤb:ℤh:b ≠ 0⊢ ⟦{ numerator := a, denominator := b, nonzero := h }⟧ = a // b
  simp [formalDiv, h]All goals completed! 🐙

Розв’язність рівності. Підказка: змініть доведення DecidableEq ℤ : TypeDecidableEq Int із попереднього розділу. Однак, оскільки формальне ділення окремо обробляє випадок нульового знаменника, може бути зручніше уникати цієї операції та працювати безпосередньо з API Quotient.{u} {α : Sort u} (s : Setoid α) : Sort uQuotient.

instance declaration uses 'sorry'Rat.decidableEq : DecidableEq Rat := by⊢ DecidableEq Rat
  sorryAll goals completed! 🐙

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

instance Rat.add_inst : Add Rat where
  add := Quotient.lift₂ (fun ⟨ a, b, h1 ⟩ ⟨ c, d, h2 ⟩ ↦ (a*d+b*c) // (b*d)) (by⊢ ∀ (a₁ b₁ a₂ b₂ : PreRat),
  a₁ ≈ a₂ →
    b₁ ≈ b₂ →
      (fun x x_1 =>
            match x with
            | { numerator := a, denominator := b, nonzero := h1 } =>
              match x_1 with
              | { numerator := c, denominator := d, nonzero := h2 } => (a * d + b * c) // (b * d))
          a₁ b₁ =
        (fun x x_1 =>
            match x with
            | { numerator := a, denominator := b, nonzero := h1 } =>
              match x_1 with
              | { numerator := c, denominator := d, nonzero := h2 } => (a * d + b * c) // (b * d))
          a₂ b₂
    intro ⟨ a, b, h1 ⟩ ⟨ c, d, h2 ⟩ ⟨ a', b', h1' ⟩ ⟨ c', d', h2' ⟩ h3 h4a:ℤb:ℤh1:b ≠ 0c:ℤd:ℤh2:d ≠ 0a':ℤb':ℤh1':b' ≠ 0c':ℤd':ℤh2':d' ≠ 0h3:{ numerator := a, denominator := b, nonzero := h1 } ≈ { numerator := a', denominator := b', nonzero := h1' }h4:{ numerator := c, denominator := d, nonzero := h2 } ≈ { numerator := c', denominator := d', nonzero := h2' }⊢ (fun x x_1 =>
      match x with
      | { numerator := a, denominator := b, nonzero := h1 } =>
        match x_1 with
        | { numerator := c, denominator := d, nonzero := h2 } => (a * d + b * c) // (b * d))
    { numerator := a, denominator := b, nonzero := h1 } { numerator := c, denominator := d, nonzero := h2 } =
  (fun x x_1 =>
      match x with
      | { numerator := a, denominator := b, nonzero := h1 } =>
        match x_1 with
        | { numerator := c, denominator := d, nonzero := h2 } => (a * d + b * c) // (b * d))
    { numerator := a', denominator := b', nonzero := h1' } { numerator := c', denominator := d', nonzero := h2' }
    simp_all [Setoid.r]a:ℤb:ℤh1:b ≠ 0c:ℤd:ℤh2:d ≠ 0a':ℤb':ℤh1':b' ≠ 0c':ℤd':ℤh2':d' ≠ 0h3:a * b' = a' * bh4:c * d' = c' * d⊢ (a * d + b * c) * (b' * d') = (a' * d' + b' * c') * (b * d)
    calc
      _ = (a*b')*d*d' + b*b'*(c*d') := bya:ℤb:ℤh1:b ≠ 0c:ℤd:ℤh2:d ≠ 0a':ℤb':ℤh1':b' ≠ 0c':ℤd':ℤh2':d' ≠ 0h3:a * b' = a' * bh4:c * d' = c' * d⊢ (a * d + b * c) * (b' * d') = a * b' * d * d' + b * b' * (c * d') ringAll goals completed! 🐙
      _ = (a'*b)*d*d' + b*b'*(c'*d) := bya:ℤb:ℤh1:b ≠ 0c:ℤd:ℤh2:d ≠ 0a':ℤb':ℤh1':b' ≠ 0c':ℤd':ℤh2':d' ≠ 0h3:a * b' = a' * bh4:c * d' = c' * d⊢ a * b' * d * d' + b * b' * (c * d') = a' * b * d * d' + b * b' * (c' * d) rw [h3, h4]All goals completed! 🐙
      _ = _ := bya:ℤb:ℤh1:b ≠ 0c:ℤd:ℤh2:d ≠ 0a':ℤb':ℤh1':b' ≠ 0c':ℤd':ℤh2':d' ≠ 0h3:a * b' = a' * bh4:c * d' = c' * d⊢ a' * b * d * d' + b * b' * (c' * d) = (a' * d' + b' * c') * (b * d) ringAll goals completed! 🐙
  )

Визначення 4.2.2 (Додавання раціональних чисел)

theorem Rat.add_eq (a c:ℤ) {b d:ℤ} (hb: b ≠ 0) (hd: d ≠ 0) :
    (a // b) + (c // d) = (a*d + b*c) // (b*d) := bya:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ a // b + c // d = (a * d + b * c) // (b * d)
  convert Quotient.lift₂_mk _ _ _ _h.e'_3.h.e'_1.h.e'_5.h.e'_5a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ a =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).numeratorh.e'_3.h.e'_1.h.e'_5.h.e'_6a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ d =
  (if h : d ≠ 0 then { numerator := c, denominator := d, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominatorh.e'_3.h.e'_1.h.e'_6.h.e'_5a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ b =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominatorh.e'_3.h.e'_1.h.e'_6.h.e'_6a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ c =
  (if h : d ≠ 0 then { numerator := c, denominator := d, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).numeratorh.e'_3.h.e'_2.h.e'_5a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ b =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominatorh.e'_3.h.e'_2.h.e'_6a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ d =
  (if h : d ≠ 0 then { numerator := c, denominator := d, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominator <;>h.e'_3.h.e'_1.h.e'_5.h.e'_5a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ a =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).numeratorh.e'_3.h.e'_1.h.e'_5.h.e'_6a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ d =
  (if h : d ≠ 0 then { numerator := c, denominator := d, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominatorh.e'_3.h.e'_1.h.e'_6.h.e'_5a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ b =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominatorh.e'_3.h.e'_1.h.e'_6.h.e'_6a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ c =
  (if h : d ≠ 0 then { numerator := c, denominator := d, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).numeratorh.e'_3.h.e'_2.h.e'_5a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ b =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominatorh.e'_3.h.e'_2.h.e'_6a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ d =
  (if h : d ≠ 0 then { numerator := c, denominator := d, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominator simp [hb, hd]All goals completed! 🐙

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

instance declaration uses 'sorry'Rat.mul_inst : Mul Rat where
  mul := Quotient.lift₂ (fun ⟨ a, b, h1 ⟩ ⟨ c, d, h2 ⟩ ↦ (a*c) // (b*d)) (by⊢ ∀ (a₁ b₁ a₂ b₂ : PreRat),
  a₁ ≈ a₂ →
    b₁ ≈ b₂ →
      (fun x x_1 =>
            match x with
            | { numerator := a, denominator := b, nonzero := h1 } =>
              match x_1 with
              | { numerator := c, denominator := d, nonzero := h2 } => (a * c) // (b * d))
          a₁ b₁ =
        (fun x x_1 =>
            match x with
            | { numerator := a, denominator := b, nonzero := h1 } =>
              match x_1 with
              | { numerator := c, denominator := d, nonzero := h2 } => (a * c) // (b * d))
          a₂ b₂ sorryAll goals completed! 🐙)

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

theorem Rat.mul_eq (a c:ℤ) {b d:ℤ} (hb: b ≠ 0) (hd: d ≠ 0) :
    (a // b) * (c // d) = (a*c) // (b*d) := bya:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ a // b * c // d = (a * c) // (b * d)
  convert Quotient.lift₂_mk _ _ _ _h.e'_3.h.e'_1.h.e'_5a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ a =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).numeratorh.e'_3.h.e'_1.h.e'_6a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ c =
  (if h : d ≠ 0 then { numerator := c, denominator := d, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).numeratorh.e'_3.h.e'_2.h.e'_5a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ b =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominatorh.e'_3.h.e'_2.h.e'_6a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ d =
  (if h : d ≠ 0 then { numerator := c, denominator := d, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominator <;>h.e'_3.h.e'_1.h.e'_5a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ a =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).numeratorh.e'_3.h.e'_1.h.e'_6a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ c =
  (if h : d ≠ 0 then { numerator := c, denominator := d, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).numeratorh.e'_3.h.e'_2.h.e'_5a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ b =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominatorh.e'_3.h.e'_2.h.e'_6a:ℤc:ℤb:ℤd:ℤhb:b ≠ 0hd:d ≠ 0⊢ d =
  (if h : d ≠ 0 then { numerator := c, denominator := d, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominator simp [hb, hd]All goals completed! 🐙

Лема 4.2.3 (Протилежний елемент коректно визначени)

instance declaration uses 'sorry'Rat.neg_inst : Neg Rat where
  neg := Quotient.lift (fun ⟨ a, b, h1 ⟩ ↦ (-a) // b) (by⊢ ∀ (a b : PreRat),
  a ≈ b →
    (fun x =>
          match x with
          | { numerator := a, denominator := b, nonzero := h1 } => (-a) // b)
        a =
      (fun x =>
          match x with
          | { numerator := a, denominator := b, nonzero := h1 } => (-a) // b)
        b sorryAll goals completed! 🐙)

Визначення 4.2.2 (Протилежний елемент раціональних чисел)

theorem Rat.neg_eq (a:ℤ) {b:ℤ} (hb: b ≠ 0) : - (a // b) = (-a) // b := bya:ℤb:ℤhb:b ≠ 0⊢ -a // b = (-a) // b
  convert Quotient.lift_mk _ _ _h.e'_3.h.e'_1.h.e'_3a:ℤb:ℤhb:b ≠ 0⊢ a =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).numeratorh.e'_3.h.e'_2a:ℤb:ℤhb:b ≠ 0⊢ b =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominator <;>h.e'_3.h.e'_1.h.e'_3a:ℤb:ℤhb:b ≠ 0⊢ a =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).numeratorh.e'_3.h.e'_2a:ℤb:ℤhb:b ≠ 0⊢ b =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominator simp [hb]All goals completed! 🐙

Вкладення цілих чисел у раціональні числа

instance Rat.instIntCast : IntCast Rat where
  intCast a := a // 1

instance Rat.instNatCast : NatCast Rat where
  natCast n := (n:ℤ) // 1

instance Rat.instOfNat {n:ℕ} : OfNat Rat n where
  ofNat := (n:ℤ) // 1

theorem Rat.coe_Int_eq (a:ℤ) : (a:Rat) = a // 1 := rfltheorem Rat.coe_Nat_eq (n:ℕ) : (n:Rat) = n // 1 := rfltheorem Rat.of_Nat_eq (n:ℕ) : (ofNat(n):Rat) = (ofNat(n):Nat) // 1 := rfl

natCast розподіляється на наступника

theorem declaration uses 'sorry'Rat.natCast_succ (n: ℕ) : ((n + 1: ℕ): Rat) = (n: Rat) + 1 := byn:ℕ⊢ ↑(n + 1) = ↑n + 1 sorryAll goals completed! 🐙

intCast розподіляється на додавання

lemma declaration uses 'sorry'Rat.intCast_add (a b:ℤ) : (a:Rat) + (b:Rat) = (a+b:ℤ) := bya:ℤb:ℤ⊢ ↑a + ↑b = ↑(a + b) sorryAll goals completed! 🐙

intCast розподіляється на множення

lemma declaration uses 'sorry'Rat.intCast_mul (a b:ℤ) : (a:Rat) * (b:Rat) = (a*b:ℤ) := bya:ℤb:ℤ⊢ ↑a * ↑b = ↑(a * b) sorryAll goals completed! 🐙

intCast комутує з взяттям протилежного елемента

lemma Rat.intCast_neg (a:ℤ) : - (a:Rat) = (-a:ℤ) := rfl

theorem declaration uses 'sorry'Rat.coe_Int_inj : Function.Injective (fun n:ℤ ↦ (n:Rat)) := by⊢ Function.Injective fun n => ↑n sorryAll goals completed! 🐙

У той час як у книзі обернене число для 0 залишається невизначеним, у Lean зручніше призначити цьому оберненому числу «сміттєве» значення; ми довільно обираємо це сміттєве значення рівним 0.

instance declaration uses 'sorry'Rat.instInv : Inv Rat where
  inv := Quotient.lift (fun ⟨ a, b, h1 ⟩ ↦ b // a) (by⊢ ∀ (a b : PreRat),
  a ≈ b →
    (fun x =>
          match x with
          | { numerator := a, denominator := b, nonzero := h1 } => b // a)
        a =
      (fun x =>
          match x with
          | { numerator := a, denominator := b, nonzero := h1 } => b // a)
        b
    sorryAll goals completed! 🐙 -- підказка: розділіть на випадки `a = 0` та `a ≠ 0`
)

lemma Rat.inv_eq (a:ℤ) {b:ℤ} (hb: b ≠ 0) : (a // b)⁻¹ = b // a := bya:ℤb:ℤhb:b ≠ 0⊢ (a // b)⁻¹ = b // a
  convert Quotient.lift_mk _ _ _h.e'_3.h.e'_1a:ℤb:ℤhb:b ≠ 0⊢ b =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominatorh.e'_3.h.e'_2a:ℤb:ℤhb:b ≠ 0⊢ a =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).numerator <;>h.e'_3.h.e'_1a:ℤb:ℤhb:b ≠ 0⊢ b =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).denominatorh.e'_3.h.e'_2a:ℤb:ℤhb:b ≠ 0⊢ a =
  (if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h }
    else { numerator := 0, denominator := 1, nonzero := formalDiv._proof_1 }).numerator simp [hb]All goals completed! 🐙

@[simp]
theorem Rat.inv_zero : (0:Rat)⁻¹ = 0 := rfl

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

instance declaration uses 'sorry'declaration uses 'sorry'Rat.addGroup_inst : AddGroup Rat :=
AddGroup.ofLeftAxioms (by⊢ ∀ (a b c : Rat), a + b + c = a + (b + c)
  -- цей доказ написан так, щоб співпадати із структурою оригінального тексту.
  intro x y zx:Raty:Ratz:Rat⊢ x + y + z = x + (y + z)
  obtain ⟨ a, b, hb, rfl ⟩ := eq_diff xintro.intro.introy:Ratz:Rata:ℤb:ℤhb:b ≠ 0⊢ a // b + y + z = a // b + (y + z)
  obtain ⟨ c, d, hd, rfl ⟩ := eq_diff yintro.intro.intro.intro.intro.introz:Rata:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0⊢ a // b + c // d + z = a // b + (c // d + z)
  obtain ⟨ e, f, hf, rfl ⟩ := eq_diff zintro.intro.intro.intro.intro.intro.intro.intro.introa:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0e:ℤf:ℤhf:f ≠ 0⊢ a // b + c // d + e // f = a // b + (c // d + e // f)
  have hbd : b*d ≠ 0 := Int.mul_ne_zero hb hdintro.intro.intro.intro.intro.intro.intro.intro.introa:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0e:ℤf:ℤhf:f ≠ 0hbd:_fvar.38578 * _fvar.38654 ≠ 0 := Int.mul_ne_zero _fvar.38600 _fvar.38672⊢ a // b + c // d + e // f = a // b + (c // d + e // f)     -- тут також можна використати `observe hbd : b*d ≠ 0`
  have hdf : d*f ≠ 0 := Int.mul_ne_zero hd hfintro.intro.intro.intro.intro.intro.intro.intro.introa:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0e:ℤf:ℤhf:f ≠ 0hbd:_fvar.38578 * _fvar.38654 ≠ 0 := Int.mul_ne_zero _fvar.38600 _fvar.38672hdf:_fvar.38654 * _fvar.38726 ≠ 0 := Int.mul_ne_zero _fvar.38672 _fvar.38744⊢ a // b + c // d + e // f = a // b + (c // d + e // f)     -- тут також можна використати `observe hdf : d*f ≠ 0`
  have hbdf : b*d*f ≠ 0 := Int.mul_ne_zero hbd hfintro.intro.intro.intro.intro.intro.intro.intro.introa:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0e:ℤf:ℤhf:f ≠ 0hbd:_fvar.38578 * _fvar.38654 ≠ 0 := Int.mul_ne_zero _fvar.38600 _fvar.38672hdf:_fvar.38654 * _fvar.38726 ≠ 0 := Int.mul_ne_zero _fvar.38672 _fvar.38744hbdf:_fvar.38578 * _fvar.38654 * _fvar.38726 ≠ 0 := Int.mul_ne_zero _fvar.38859 _fvar.38744⊢ a // b + c // d + e // f = a // b + (c // d + e // f) -- тут також можна використати `observe hbdf : b*d*f ≠ 0`
  rw [add_eq _ _ hb hd, add_eq _ _ hbd hf, add_eq _ _ hd hf,
      add_eq _ _ hb hdf, ←mul_assoc b, eq _ _ hbdf hbdf]intro.intro.intro.intro.intro.intro.intro.intro.introa:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0e:ℤf:ℤhf:f ≠ 0hbd:_fvar.38578 * _fvar.38654 ≠ 0 := Int.mul_ne_zero _fvar.38600 _fvar.38672hdf:_fvar.38654 * _fvar.38726 ≠ 0 := Int.mul_ne_zero _fvar.38672 _fvar.38744hbdf:_fvar.38578 * _fvar.38654 * _fvar.38726 ≠ 0 := Int.mul_ne_zero _fvar.38859 _fvar.38744⊢ ((a * d + b * c) * f + b * d * e) * (b * d * f) = (a * (d * f) + b * (c * f + d * e)) * (b * d * f)
  ringAll goals completed! 🐙
)
 (by⊢ ∀ (a : Rat), 0 + a = a sorryAll goals completed! 🐙) (by⊢ ∀ (a : Rat), -a + a = 0 sorryAll goals completed! 🐙)

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

instance declaration uses 'sorry'Rat.instAddCommGroup : AddCommGroup Rat where
  add_comm := by⊢ ∀ (a b : Rat), a + b = b + a sorryAll goals completed! 🐙

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

instance declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Rat.instCommMonoid : CommMonoid Rat where
  mul_comm := by⊢ ∀ (a b : Rat), a * b = b * a sorryAll goals completed! 🐙
  mul_assoc := by⊢ ∀ (a b c : Rat), a * b * c = a * (b * c) sorryAll goals completed! 🐙
  one_mul := by⊢ ∀ (a : Rat), 1 * a = a sorryAll goals completed! 🐙
  mul_one := by⊢ ∀ (a : Rat), a * 1 = a sorryAll goals completed! 🐙

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

instance declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Rat.instCommRing : CommRing Rat where
  left_distrib := by⊢ ∀ (a b c : Rat), a * (b + c) = a * b + a * c sorryAll goals completed! 🐙
  right_distrib := by⊢ ∀ (a b c : Rat), (a + b) * c = a * c + b * c sorryAll goals completed! 🐙
  zero_mul := by⊢ ∀ (a : Rat), 0 * a = 0 sorryAll goals completed! 🐙
  mul_zero := by⊢ ∀ (a : Rat), a * 0 = 0 sorryAll goals completed! 🐙
  mul_assoc := by⊢ ∀ (a b c : Rat), a * b * c = a * (b * c) sorryAll goals completed! 🐙
  -- Зазвичай `CommRing` згенерує екземпляр `natCast` та доведення для цього.
  -- Однак ми використовуємо власний `natCast`, для якого `natCast_succ` не можна
  -- автоматично довести за допомогою `rfl`. На щастя, ми вже це довели.
  natCast_succ := natCast_succ

instance Rat.instRatCast : RatCast Rat where
  ratCast q := q.num // q.den

theorem declaration uses 'sorry'Rat.ratCast_inj : Function.Injective (fun n:ℚ ↦ (n:Rat)) := by⊢ Function.Injective fun n => ↑n sorryAll goals completed! 🐙

theorem Rat.coe_Rat_eq (a:ℤ) {b:ℤ} (hb: b ≠ 0) : (a/b:ℚ) = a // b := bya:ℤb:ℤhb:b ≠ 0⊢ ↑(↑a / ↑b) = a // b
  set q := (a/b:ℚ)a:ℤb:ℤhb:b ≠ 0q:ℚ := ↑_fvar.43387 / ↑_fvar.43388⊢ ↑q = a // b
  set num :ℤ := q.numa:ℤb:ℤhb:b ≠ 0q:ℚ := ↑_fvar.43387 / ↑_fvar.43388num:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ ↑q = a // b
  set den :ℤ := (q.den:ℤ)a:ℤb:ℤhb:b ≠ 0q:ℚ := ↑_fvar.43387 / ↑_fvar.43388num:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ ↑q = a // b
  have hden : den ≠ 0 := bya:ℤb:ℤhb:b ≠ 0⊢ ↑(↑a / ↑b) = a // b simp [den, q.den_nz]All goals completed! 🐙
  change num // den = a // ba:ℤb:ℤhb:b ≠ 0q:ℚ := ↑_fvar.43387 / ↑_fvar.43388num:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:_fvar.43699 ≠ 0 := ?_mvar.43808⊢ num // den = a // b
  rw [eq _ _ hden hb]a:ℤb:ℤhb:b ≠ 0q:ℚ := ↑_fvar.43387 / ↑_fvar.43388num:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:_fvar.43699 ≠ 0 := ?_mvar.43808⊢ num * b = a * den
  qifya:ℤb:ℤhb:b ≠ 0q:ℚ := ↑_fvar.43387 / ↑_fvar.43388num:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:_fvar.43699 ≠ 0 := ?_mvar.43808⊢ ↑num * ↑b = ↑a * ↑den
  have hq : num / den = q := Rat.num_div_den qa:ℤb:ℤhb:b ≠ 0q:ℚ := ↑_fvar.43387 / ↑_fvar.43388num:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:_fvar.43699 ≠ 0 := ?_mvar.43808hq:↑_fvar.43609 / ↑_fvar.43699 = _fvar.43551 := Rat.num_div_den _fvar.43551⊢ ↑num * ↑b = ↑a * ↑den
  rwa [div_eq_div_iff]a:ℤb:ℤhb:b ≠ 0q:ℚ := ↑_fvar.43387 / ↑_fvar.43388num:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:_fvar.43699 ≠ 0 := ?_mvar.43808hq:↑num * ↑b = ↑a * ↑den⊢ ↑num * ↑b = ↑a * ↑denhba:ℤb:ℤhb:b ≠ 0q:ℚ := ↑_fvar.43387 / ↑_fvar.43388num:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:_fvar.43699 ≠ 0 := ?_mvar.43808hq:↑_fvar.43609 / ↑_fvar.43699 = _fvar.43551 := Rat.num_div_den _fvar.43551⊢ ↑den ≠ 0hda:ℤb:ℤhb:b ≠ 0q:ℚ := ↑_fvar.43387 / ↑_fvar.43388num:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:_fvar.43699 ≠ 0 := ?_mvar.43808hq:↑_fvar.43609 / ↑_fvar.43699 = _fvar.43551 := Rat.num_div_den _fvar.43551⊢ ↑b ≠ 0 at hq <;>hba:ℤb:ℤhb:b ≠ 0q:ℚ := ↑_fvar.43387 / ↑_fvar.43388num:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:_fvar.43699 ≠ 0 := ?_mvar.43808hq:↑_fvar.43609 / ↑_fvar.43699 = _fvar.43551 := Rat.num_div_den _fvar.43551⊢ ↑den ≠ 0hda:ℤb:ℤhb:b ≠ 0q:ℚ := ↑_fvar.43387 / ↑_fvar.43388num:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:_fvar.43699 ≠ 0 := ?_mvar.43808hq:↑_fvar.43609 / ↑_fvar.43699 = _fvar.43551 := Rat.num_div_den _fvar.43551⊢ ↑b ≠ 0 simp [hden, hb]All goals completed! 🐙

Default definition of division

instance Rat.instDivInvMonoid : DivInvMonoid Rat where

theorem Rat.div_eq (q r:Rat) : q/r = q * r⁻¹ := byq:Ratr:Rat⊢ q / r = q * r⁻¹ rflAll goals completed! 🐙

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

instance declaration uses 'sorry'declaration uses 'sorry'Rat.instField : Field Rat where
  exists_pair_ne := by⊢ ∃ x y, x ≠ y sorryAll goals completed! 🐙
  mul_inv_cancel := by⊢ ∀ (a : Rat), a ≠ 0 → a * a⁻¹ = 1 sorryAll goals completed! 🐙
  inv_zero := rfl
  ratCast_def := by⊢ ∀ (q : ℚ), ↑q = ↑q.num / ↑q.den
    intro qq:ℚ⊢ ↑q = ↑q.num / ↑q.den
    set num := q.numq:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ ↑q = ↑num / ↑q.den
    set den := q.denq:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ ↑q = ↑num / ↑den
    have hden : (den:ℤ) ≠ 0 := by⊢ ∀ (q : ℚ), ↑q = ↑q.num / ↑q.den simp [den, q.den_nz]All goals completed! 🐙
    rw [← Rat.num_div_den q]q:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:↑_fvar.47889 ≠ 0 := ?_mvar.48005⊢ ↑(↑q.num / ↑q.den) = ↑num / ↑den
    convert coe_Rat_eq _ hdenh.e'_3q:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:↑_fvar.47889 ≠ 0 := ?_mvar.48005⊢ ↑num / ↑den = q.num // ↑den
    rw [coe_Int_eq, coe_Nat_eq, div_eq, inv_eq, mul_eq, eq]h.e'_3q:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:↑_fvar.47889 ≠ 0 := ?_mvar.48005⊢ num * 1 * ↑den = q.num * (1 * ↑den)h.e'_3.hbq:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:↑_fvar.47889 ≠ 0 := ?_mvar.48005⊢ 1 * ↑den ≠ 0h.e'_3.hdq:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:↑_fvar.47889 ≠ 0 := ?_mvar.48005⊢ ↑den ≠ 0h.e'_3.hbq:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:↑_fvar.47889 ≠ 0 := ?_mvar.48005⊢ 1 ≠ 0h.e'_3.hdq:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:↑_fvar.47889 ≠ 0 := ?_mvar.48005⊢ ↑den ≠ 0h.e'_3.hbq:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:↑_fvar.47889 ≠ 0 := ?_mvar.48005⊢ 1 ≠ 0 <;>h.e'_3q:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:↑_fvar.47889 ≠ 0 := ?_mvar.48005⊢ num * 1 * ↑den = q.num * (1 * ↑den)h.e'_3.hbq:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:↑_fvar.47889 ≠ 0 := ?_mvar.48005⊢ 1 * ↑den ≠ 0h.e'_3.hdq:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:↑_fvar.47889 ≠ 0 := ?_mvar.48005⊢ ↑den ≠ 0h.e'_3.hbq:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:↑_fvar.47889 ≠ 0 := ?_mvar.48005⊢ 1 ≠ 0h.e'_3.hdq:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:↑_fvar.47889 ≠ 0 := ?_mvar.48005⊢ ↑den ≠ 0h.e'_3.hbq:ℚnum:ℤ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)den:ℕ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hden:↑_fvar.47889 ≠ 0 := ?_mvar.48005⊢ 1 ≠ 0 simp [num, den, q.den_nz]All goals completed! 🐙
  qsmul := _
  nnqsmul := _

declaration uses 'sorry'example : (3//4) / (5//6) = 9 // 10 := by⊢ 3 // 4 / 5 // 6 = 9 // 10 sorryAll goals completed! 🐙

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

theorem Rat.sub_eq (a b:Rat) : a - b = a + (-b) := bya:Ratb:Rat⊢ a - b = a + -b rflAll goals completed! 🐙

def declaration uses 'sorry'declaration uses 'sorry'Rat.coe_int_hom : ℤ →+* Rat where
  toFun n := (n:Rat)
  map_zero' := rfl
  map_one' := rfl
  map_add' := by⊢ ∀ (x y : ℤ), ↑(x + y) = ↑x + ↑y sorryAll goals completed! 🐙
  map_mul' := by⊢ ∀ (x y : ℤ), ↑(x * y) = ↑x * ↑y sorryAll goals completed! 🐙

Визначення 4.2.6 (позитивність)

def Rat.isPos (q:Rat) : Prop := ∃ a b:ℤ, a > 0 ∧ b > 0 ∧ q = a/b

Визначення 4.2.6 (негативність)

def Rat.isNeg (q:Rat) : Prop := ∃ r:Rat, r.isPos ∧ q = -r

Лема 4.2.7 (трихотомія раціональних чисел) / Вправа 4.2.4

theorem declaration uses 'sorry'Rat.trichotomous (x:Rat) : x = 0 ∨ x.isPos ∨ x.isNeg := byx:Rat⊢ x = 0 ∨ x.isPos ∨ x.isNeg sorryAll goals completed! 🐙

Лема 4.2.7 (трихотомія раціональних чисел) / Вправа 4.2.4

theorem declaration uses 'sorry'Rat.not_zero_and_pos (x:Rat) : ¬(x = 0 ∧ x.isPos) := byx:Rat⊢ ¬(x = 0 ∧ x.isPos) sorryAll goals completed! 🐙

Лема 4.2.7 (трихотомія раціональних чисел) / Вправа 4.2.4

theorem declaration uses 'sorry'Rat.not_zero_and_neg (x:Rat) : ¬(x = 0 ∧ x.isNeg) := byx:Rat⊢ ¬(x = 0 ∧ x.isNeg) sorryAll goals completed! 🐙

Лема 4.2.7 (трихотомія раціональних чисел) / Вправа 4.2.4

theorem declaration uses 'sorry'Rat.not_pos_and_neg (x:Rat) : ¬(x.isPos ∧ x.isNeg) := byx:Rat⊢ ¬(x.isPos ∧ x.isNeg) sorryAll goals completed! 🐙

Визначення 4.2.8 (Порядок раціональних чисел)

instance Rat.instLT : LT Rat where
  lt x y := (x-y).isNeg

Визначення 4.2.8 (Порядок раціональних чисел)

instance Rat.instLE : LE Rat where
  le x y := (x < y) ∨ (x = y)

theorem Rat.lt_iff (x y:Rat) : x < y ↔ (x-y).isNeg := byx:Raty:Rat⊢ x < y ↔ (x - y).isNeg rflAll goals completed! 🐙

theorem Rat.le_iff (x y:Rat) : x ≤ y ↔ (x < y) ∨ (x = y) := byx:Raty:Rat⊢ x ≤ y ↔ x < y ∨ x = y rflAll goals completed! 🐙

theorem declaration uses 'sorry'Rat.gt_iff (x y:Rat) : x > y ↔ (x-y).isPos := byx:Raty:Rat⊢ x > y ↔ (x - y).isPos sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Rat.ge_iff (x y:Rat) : x ≥ y ↔ (x > y) ∨ (x = y) := byx:Raty:Rat⊢ x ≥ y ↔ x > y ∨ x = y sorryAll goals completed! 🐙

Твердження 4.2.9(a) (трихотомія порядку) / Вправа 4.2.5

theorem declaration uses 'sorry'Rat.trichotomous' (x y:Rat) : x > y ∨ x < y ∨ x = y := byx:Raty:Rat⊢ x > y ∨ x < y ∨ x = y sorryAll goals completed! 🐙

Твердження 4.2.9(a) (трихотомія порядку) / Вправа 4.2.5

theorem declaration uses 'sorry'Rat.not_gt_and_lt (x y:Rat) : ¬ (x > y ∧ x < y):= byx:Raty:Rat⊢ ¬(x > y ∧ x < y) sorryAll goals completed! 🐙

Твердження 4.2.9(a) (трихотомія порядку) / Вправа 4.2.5

theorem declaration uses 'sorry'Rat.not_gt_and_eq (x y:Rat) : ¬ (x > y ∧ x = y):= byx:Raty:Rat⊢ ¬(x > y ∧ x = y) sorryAll goals completed! 🐙

Твердження 4.2.9(a) (трихотомія порядку) / Вправа 4.2.5

theorem declaration uses 'sorry'Rat.not_lt_and_eq (x y:Rat) : ¬ (x < y ∧ x = y):= byx:Raty:Rat⊢ ¬(x < y ∧ x = y) sorryAll goals completed! 🐙

Твердження 4.2.9(b) (порядок є антисиметричним) / Вправа 4.2.5

theorem declaration uses 'sorry'Rat.antisymm (x y:Rat) : x < y ↔ y > x := byx:Raty:Rat⊢ x < y ↔ y > x sorryAll goals completed! 🐙

Твердження 4.2.9(c) (порядок є транзитивним) / Вправа 4.2.5

theorem declaration uses 'sorry'Rat.lt_trans {x y z:Rat} (hxy: x < y) (hyz: y < z) : x < z := byx:Raty:Ratz:Rathxy:x < yhyz:y < z⊢ x < z sorryAll goals completed! 🐙

Твердження 4.2.9(d) (додавання зберігає порядок) / Вправа 4.2.5

theorem declaration uses 'sorry'Rat.add_lt_add_right {x y:Rat} (z:Rat) (hxy: x < y) : x + z < y + z := byx:Raty:Ratz:Rathxy:x < y⊢ x + z < y + z sorryAll goals completed! 🐙

Твердження 4.2.9(e) (множення на додатне число зберігає порядок) / Вправа 4.2.5

theorem declaration uses 'sorry'Rat.mul_lt_mul_right {x y z:Rat} (hxy: x < y) (hz: z.isPos) : x * z < y * z := byx:Raty:Ratz:Rathxy:x < yhz:z.isPos⊢ x * z < y * z sorryAll goals completed! 🐙

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

instance declaration uses 'sorry'declaration uses 'sorry'Rat.decidableRel : DecidableRel (·≤ ·: Rat → Rat → Prop) := by⊢ DecidableRel fun x1 x2 => x1 ≤ x2
  intro n mn:Ratm:Rat⊢ Decidable ((fun x1 x2 => x1 ≤ x2) n m)
  have : ∀ (n:PreRat) (m: PreRat),
      Decidable (Quotient.mk PreRat.instSetoid n ≤ Quotient.mk PreRat.instSetoid m) := by⊢ DecidableRel fun x1 x2 => x1 ≤ x2
    intro ⟨ a,b,hb ⟩ ⟨ c,d,hd ⟩n:Ratm:Rata:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0⊢ Decidable
  (⟦{ numerator := a, denominator := b, nonzero := hb }⟧ ≤ ⟦{ numerator := c, denominator := d, nonzero := hd }⟧)
    -- на цьому етапі ціль фактично `Decidable(a//b ≤ c//d)`, але існують технічні
    -- проблеми через «сміттєве» значення формального ділення, коли знаменник дорівнює нулю.
    -- Може бути зручніше уникати формального ділення та працювати безпосередньо з `Quotient.mk`.
    cases (0:ℤ).decLe (b*d) with
      | isTrue hbd =>isTruen:Ratm:Rata:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0hbd:0 ≤ b * d⊢ Decidable
  (⟦{ numerator := a, denominator := b, nonzero := hb }⟧ ≤ ⟦{ numerator := c, denominator := d, nonzero := hd }⟧)
        cases (a * d).decLe (b * c) with
          | isTrue h =>isTrue.isTruen:Ratm:Rata:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0hbd:0 ≤ b * dh:a * d ≤ b * c⊢ Decidable
  (⟦{ numerator := a, denominator := b, nonzero := hb }⟧ ≤ ⟦{ numerator := c, denominator := d, nonzero := hd }⟧)
            apply isTrueisTrue.isTrue.hn:Ratm:Rata:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0hbd:0 ≤ b * dh:a * d ≤ b * c⊢ ⟦{ numerator := a, denominator := b, nonzero := hb }⟧ ≤ ⟦{ numerator := c, denominator := d, nonzero := hd }⟧
            sorryAll goals completed! 🐙
          | isFalse h =>isTrue.isFalsen:Ratm:Rata:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0hbd:0 ≤ b * dh:¬a * d ≤ b * c⊢ Decidable
  (⟦{ numerator := a, denominator := b, nonzero := hb }⟧ ≤ ⟦{ numerator := c, denominator := d, nonzero := hd }⟧)
            apply isFalseisTrue.isFalse.hn:Ratm:Rata:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0hbd:0 ≤ b * dh:¬a * d ≤ b * c⊢ ¬⟦{ numerator := a, denominator := b, nonzero := hb }⟧ ≤ ⟦{ numerator := c, denominator := d, nonzero := hd }⟧
            sorryAll goals completed! 🐙
      | isFalse hbd =>isFalsen:Ratm:Rata:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0hbd:¬0 ≤ b * d⊢ Decidable
  (⟦{ numerator := a, denominator := b, nonzero := hb }⟧ ≤ ⟦{ numerator := c, denominator := d, nonzero := hd }⟧)
        cases (b * c).decLe (a * d) with
          | isTrue h =>isFalse.isTruen:Ratm:Rata:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0hbd:¬0 ≤ b * dh:b * c ≤ a * d⊢ Decidable
  (⟦{ numerator := a, denominator := b, nonzero := hb }⟧ ≤ ⟦{ numerator := c, denominator := d, nonzero := hd }⟧)
            apply isTrueisFalse.isTrue.hn:Ratm:Rata:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0hbd:¬0 ≤ b * dh:b * c ≤ a * d⊢ ⟦{ numerator := a, denominator := b, nonzero := hb }⟧ ≤ ⟦{ numerator := c, denominator := d, nonzero := hd }⟧
            sorryAll goals completed! 🐙
          | isFalse h =>isFalse.isFalsen:Ratm:Rata:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0hbd:¬0 ≤ b * dh:¬b * c ≤ a * d⊢ Decidable
  (⟦{ numerator := a, denominator := b, nonzero := hb }⟧ ≤ ⟦{ numerator := c, denominator := d, nonzero := hd }⟧)
            apply isFalseisFalse.isFalse.hn:Ratm:Rata:ℤb:ℤhb:b ≠ 0c:ℤd:ℤhd:d ≠ 0hbd:¬0 ≤ b * dh:¬b * c ≤ a * d⊢ ¬⟦{ numerator := a, denominator := b, nonzero := hb }⟧ ≤ ⟦{ numerator := c, denominator := d, nonzero := hd }⟧
            sorryAll goals completed! 🐙
  exact Quotient.recOnSubsingleton₂ n m thisAll goals completed! 🐙

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

instance declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Rat.instLinearOrder : LinearOrder Rat where
  le_refl := sorry
  le_trans := sorry
  lt_iff_le_not_ge := sorry
  le_antisymm := sorry
  le_total := sorry
  toDecidableLE := decidableRel

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

instance declaration uses 'sorry'Rat.instIsStrictOrderedRing : IsStrictOrderedRing Rat where
  add_le_add_left := by⊢ ∀ (a b : Rat), a ≤ b → ∀ (c : Rat), c + a ≤ c + b sorryAll goals completed! 🐙
  add_le_add_right := by⊢ ∀ (a b : Rat), a ≤ b → ∀ (c : Rat), a + c ≤ b + c sorryAll goals completed! 🐙
  mul_lt_mul_of_pos_left := by⊢ ∀ (a b c : Rat), a < b → 0 < c → c * a < c * b sorryAll goals completed! 🐙
  mul_lt_mul_of_pos_right := by⊢ ∀ (a b c : Rat), a < b → 0 < c → a * c < b * c sorryAll goals completed! 🐙
  le_of_add_le_add_left := by⊢ ∀ (a b c : Rat), a + b ≤ a + c → b ≤ c sorryAll goals completed! 🐙
  zero_le_one := by⊢ 0 ≤ 1 sorryAll goals completed! 🐙

Вправа 4.2.6

theorem declaration uses 'sorry'Rat.mul_lt_mul_right_of_neg (x y z:Rat) (hxy: x < y) (hz: z.isNeg) : x * z > y * z := byx:Raty:Ratz:Rathxy:x < yhz:z.isNeg⊢ x * z > y * z
  sorryAll goals completed! 🐙

Не в підручнику: створіть еквівалентність між Section_4_2.Rat : TypeRat та ℚ : Typeℚ. Це вимагає певного знайомства з API для версії раціональних чисел у Mathlib.

abbrev declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Rat.equivRat : Rat ≃ ℚ where
  toFun := Quotient.lift (fun ⟨ a, b, h ⟩ ↦ a / b) (by⊢ ∀ (a b : PreRat),
  a ≈ b →
    (fun x =>
          match x with
          | { numerator := a, denominator := b, nonzero := h } => ↑a / ↑b)
        a =
      (fun x =>
          match x with
          | { numerator := a, denominator := b, nonzero := h } => ↑a / ↑b)
        b
    sorryAll goals completed! 🐙)
  invFun := fun n: ℚ ↦ (n:Rat)
  left_inv n := sorry
  right_inv n := sorry

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

abbrev declaration uses 'sorry'Rat.equivRat_order : Rat ≃o ℚ where
  toEquiv := equivRat
  map_rel_iff' := by⊢ ∀ {a b : Rat}, equivRat a ≤ equivRat b ↔ a ≤ b sorryAll goals completed! 🐙

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

abbrev declaration uses 'sorry'declaration uses 'sorry'Rat.equivRat_ring : Rat ≃+* ℚ where
  toEquiv := equivRat
  map_add' := by⊢ ∀ (x y : Rat), equivRat.toFun (x + y) = equivRat.toFun x + equivRat.toFun y sorryAll goals completed! 🐙
  map_mul' := by⊢ ∀ (x y : Rat), equivRat.toFun (x * y) = equivRat.toFun x * equivRat.toFun y sorryAll goals completed! 🐙

(Не в підручнику) Раціональні числа з підручника ізоморфні (як поле) до раціональних чисел Mathlib.

def Rat.equivRat_ring_symm : ℚ ≃+* Rat := Rat.equivRat_ring.symm

end Section_4_2