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 forvonNeumann o
. It is scoped in theZFSet
namespace.
@[irreducible]
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_succ
:V_ (succ a) = powerset (V_ a)
vonNeumann_of_isSuccPrelimit
:IsSuccPrelimit a → V_ a = ⋃ b < a, V_ b
Equations
- ZFSet.vonNeumann o = ⋃₀ ZFSet.range fun (a : ↑(Set.Iio o)) => (ZFSet.vonNeumann ↑a).powerset
Instances For
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_succ
:V_ (succ a) = powerset (V_ a)
vonNeumann_of_isSuccPrelimit
:IsSuccPrelimit a → V_ a = ⋃ b < a, V_ b
Equations
- ZFSet.termV_ = Lean.ParserDescr.node `ZFSet.termV_ 1024 (Lean.ParserDescr.symbol "V_ ")
Instances For
@[irreducible]
@[irreducible]
Every set is in some element of the von Neumann hierarchy.
@[simp, irreducible]
@[simp]
@[simp]
theorem
ZFSet.mem_vonNeumann_of_subset
{o : Ordinal.{u}}
{x y : ZFSet.{u}}
(h : x ⊆ y)
(hy : y ∈ vonNeumann o)
:
theorem
GCongr.ZFSet.vonNeumann_inj
{a b : Ordinal.{u}}
:
a = b → ZFSet.vonNeumann a = ZFSet.vonNeumann b
Alias of the reverse direction of ZFSet.vonNeumann_inj
.
@[simp]