Analysis I, Chapter 3 epilogue: Connections with ZFSet

In this epilogue we show that the ZFSet type in Mathlib (derived as a quotient from the PSet type) can be used to create models of the `SetTheory' class studied in this chapter, so long as we work in a universe of level at least 1. The constructions here are due to Edward van de Meent; see 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

A preliminary lemma about PSet: their natural numbers are ordered by membership.

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

Another preliminary lemma: Natural numbers in PSet can only be equivalent if they are equal.

noncomputable def ZFSet.nat_equiv : ℕ ≃ ↥omega

Using the above lemmas, we can create a bijection between ZFSet.omega and the natural numbers.

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

Show that ZFSet obeys the Chapter3.SetTheory axioms. Most of these axioms were essentially already established in Mathlib and are relatively routine to transfer over; the equivalence of ZF.omega and Nat being the trickiest one in content (and the power set axiom also requiring some technical manipulation).

Equations

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