Theorems · Definition · logic and foundations

ZFSet.vonNeumann

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

Defined in

Mathlib.SetTheory.ZFC.VonNeumann

Cited by

25 results in Mathlib

Foundations

Depth 43 from the axioms · uses propext, Classical.choice, Quot.sound