Аналіз I, Розділ 3.6, Епілог: Зв’язки із ZFSet

У цьому епілозі ми показуємо, що тип ZFSet у Mathlib (отриманий як частка від типу PSet) можна використовувати для створення моделей класу SetTheory', вивченого в цьому розділі, за умови роботи у всесвіті рівня щонайменше 1. Конструкції тут належать Едварду ван де Менту; див. https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Can.20this.20proof.20related.20to.20Set.20replacement.20be.20shorter.3F/near/527305173

theorem PSet.ofNat_mem_ofNat_of_lt (m n : ℕ) : n < m → ofNat n ∈ ofNat m

Вступна лема про PSet: їхні натуральні числа впорядковані за відношенням належності.

theorem PSet.mem_ofNat_iff (n m : ℕ) : ofNat n ∈ ofNat m ↔ n < m

theorem PSet.eq_of_ofNat_equiv_ofNat (n m : ℕ) : (ofNat n).Equiv (ofNat m) → n = m

Ще одна вступна лема: натуральні числа в PSet можуть бути еквівалентними лише тоді, коли вони рівні.

noncomputable def ZFSet.nat_equiv : ℕ ≃ ↥omega

Використовуючи наведені вище леми, ми можемо створити бієкцію між ZFSet.omega та натуральними числами.

Equations

• ZFSet.nat_equiv = Equiv.ofBijective (fun (n : ℕ) => ⟨ZFSet.mk (PSet.ofNat n), ⋯⟩) ZFSet.nat_equiv._proof_2

noncomputable instance ZFSet.inst_SetTheory : Chapter3.SetTheory

Покажіть, що ZFSet задовольняє аксіоми Chapter3.SetTheory. Більшість цих аксіом фактично вже були встановлені в Mathlib і їх відносно легко перенести; найбільш складним за змістом є еквівалентність ZF.omega та Nat (а аксіома множини всіх підмножин також потребує деяких технічних маніпуляцій).

Equations

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