Von Neumann hierarchy

This file defines the von Neumann hierarchy of sets V_ o for ordinal o, which is recursively defined so that V_ a = ⋃ b < a, powerset (V_ b). This stratifies the universal class, in the sense that ⋃ o, V_ o = univ.

Notation

• V_ o is notation for vonNeumann o. It is scoped in the ZFSet namespace.

@[irreducible]

noncomputable def ZFSet.vonNeumann (o : Ordinal.{u}) : ZFSet.{u}

The von Neumann hierarchy is defined so that V_ o is the union of the powersets of all V_ a for a < o. It satisfies the following properties:

• vonNeumann_zero: V_ 0 = ∅
• vonNeumann_add_one: V_ (a + 1) = powerset (V_ a)
• vonNeumann_of_isSuccPrelimit: IsSuccPrelimit a → V_ a = ⋃ b < a, V_ b

def ZFSet.termV_ : Lean.ParserDescr

The von Neumann hierarchy is defined so that V_ o is the union of the powersets of all V_ a for a < o. It satisfies the following properties:

• vonNeumann_zero: V_ 0 = ∅
• vonNeumann_add_one: V_ (a + 1) = powerset (V_ a)
• vonNeumann_of_isSuccPrelimit: IsSuccPrelimit a → V_ a = ⋃ b < a, V_ b

theorem ZFSet.mem_vonNeumann' {o : Ordinal.{u}} {x : ZFSet.{u}} : x ∈ vonNeumann o ↔ ∃ a < o, x ⊆ vonNeumann a

@[irreducible]

theorem ZFSet.isTransitive_vonNeumann (o : Ordinal.{u_1}) : (vonNeumann o).IsTransitive

theorem ZFSet.vonNeumann_mem_of_lt {a b : Ordinal.{u}} (h : a < b) : vonNeumann a ∈ vonNeumann b

theorem ZFSet.vonNeumann_subset_of_le {a b : Ordinal.{u}} (h : a ≤ b) : vonNeumann a ⊆ vonNeumann b

@[irreducible]

theorem ZFSet.subset_vonNeumann {o : Ordinal.{u_1}} {x : ZFSet.{u_1}} : x ⊆ vonNeumann o ↔ x.rank ≤ o

theorem ZFSet.subset_vonNeumann_self (x : ZFSet.{u_1}) : x ⊆ vonNeumann x.rank

theorem ZFSet.mem_vonNeumann {o : Ordinal.{u}} {x : ZFSet.{u}} : x ∈ vonNeumann o ↔ x.rank < o

theorem ZFSet.mem_vonNeumann_succ (x : ZFSet.{u_1}) : x ∈ vonNeumann (Order.succ x.rank)

theorem ZFSet.exists_mem_vonNeumann (x : ZFSet.{u_1}) : ∃ (o : Ordinal.{u_1}), x ∈ vonNeumann o

Every set is in some element of the von Neumann hierarchy.

@[simp, irreducible]

theorem ZFSet.rank_vonNeumann (o : Ordinal.{u_1}) : (vonNeumann o).rank = o

@[simp]

theorem ZFSet.vonNeumann_mem_vonNeumann_iff {a b : Ordinal.{u}} : vonNeumann a ∈ vonNeumann b ↔ a < b

@[simp]

theorem ZFSet.vonNeumann_subset_vonNeumann_iff {a b : Ordinal.{u}} : vonNeumann a ⊆ vonNeumann b ↔ a ≤ b

theorem ZFSet.mem_vonNeumann_of_subset {o : Ordinal.{u}} {x y : ZFSet.{u}} (h : x ⊆ y) (hy : y ∈ vonNeumann o) : x ∈ vonNeumann o

theorem ZFSet.vonNeumann_strictMono : StrictMono vonNeumann

theorem ZFSet.vonNeumann_injective : Function.Injective vonNeumann

@[simp]

theorem ZFSet.vonNeumann_inj {a b : Ordinal.{u}} : vonNeumann a = vonNeumann b ↔ a = b

@[simp]

theorem ZFSet.vonNeumann_zero : vonNeumann 0 = ∅

@[simp]

theorem ZFSet.vonNeumann_add_one (o : Ordinal.{u_1}) : vonNeumann (o + 1) = (vonNeumann o).powerset

theorem ZFSet.vonNeumann_succ (o : Ordinal.{u_1}) : vonNeumann (Order.succ o) = (vonNeumann o).powerset

theorem ZFSet.vonNeumann_of_isSuccPrelimit {o : Ordinal.{u}} (h : Order.IsSuccPrelimit o) : vonNeumann o = iUnion fun (a : ↑(Set.Iio o)) => vonNeumann ↑a

theorem ZFSet.iUnion_vonNeumann : ⋃ (o : Ordinal.{u_1}), ↑(vonNeumann o) = Class.univ

theorem Ordinal.toZFSet_subset_vonNeumann (o : Ordinal.{u_1}) : o.toZFSet ⊆ ZFSet.vonNeumann o

theorem Ordinal.card_le_card_vonNeumann (o : Ordinal.{u_1}) : o.card ≤ (ZFSet.vonNeumann o).card

theorem ZFSet.card_vonNeumann (o : Ordinal.{u}) : (vonNeumann o).card = Cardinal.preBeth o