Documentation

Mathlib.SetTheory.ZFC.VonNeumann

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 #

@[irreducible]
noncomputable def ZFSet.vonNeumann (o : Ordinal.{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:

Equations
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:

    Equations
    Instances For
      @[irreducible]

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

      @[simp, irreducible]

      Alias of the reverse direction of ZFSet.vonNeumann_inj.