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 #

source
@[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:

Equations
Instances For
    source
    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:

    Equations
    Instances For
      source
      theorem ZFSet.mem_vonNeumann' {o : Ordinal.{u}} {x : ZFSet.{u}} :
      x ∈ vonNeumann o ↔ ∃ a < o, x ⊆ vonNeumann a
      source
      @[irreducible]
      theorem ZFSet.isTransitive_vonNeumann (o : Ordinal.{u_1}) :
      (vonNeumann o).IsTransitive
      source
      theorem ZFSet.vonNeumann_mem_of_lt {a b : Ordinal.{u}} (h : a < b) :
      vonNeumann a ∈ vonNeumann b
      source
      theorem ZFSet.vonNeumann_subset_of_le {a b : Ordinal.{u}} (h : a ≤ b) :
      vonNeumann a ⊆ vonNeumann b
      source
      @[irreducible]
      theorem ZFSet.subset_vonNeumann {o : Ordinal.{u_1}} {x : ZFSet.{u_1}} :
      x ⊆ vonNeumann o ↔ x.rank ≤ o
      source
      theorem ZFSet.subset_vonNeumann_self (x : ZFSet.{u_1}) :
      x ⊆ vonNeumann x.rank
      source
      theorem ZFSet.mem_vonNeumann {o : Ordinal.{u}} {x : ZFSet.{u}} :
      x ∈ vonNeumann o ↔ x.rank < o
      source
      theorem ZFSet.mem_vonNeumann_succ (x : ZFSet.{u_1}) :
      x ∈ vonNeumann (Order.succ x.rank)
      source
      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.

      source
      @[simp, irreducible]
      theorem ZFSet.rank_vonNeumann (o : Ordinal.{u_1}) :
      (vonNeumann o).rank = o
      source
      @[simp]
      theorem ZFSet.vonNeumann_mem_vonNeumann_iff {a b : Ordinal.{u}} :
      vonNeumann a ∈ vonNeumann b ↔ a < b
      source
      @[simp]
      theorem ZFSet.vonNeumann_subset_vonNeumann_iff {a b : Ordinal.{u}} :
      vonNeumann a ⊆ vonNeumann b ↔ a ≤ b
      source
      theorem ZFSet.mem_vonNeumann_of_subset {o : Ordinal.{u}} {x y : ZFSet.{u}} (h : x ⊆ y) (hy : y ∈ vonNeumann o) :
      x ∈ vonNeumann o
      source
      theorem ZFSet.vonNeumann_strictMono :
      StrictMono vonNeumann
      source
      theorem ZFSet.vonNeumann_injective :
      Function.Injective vonNeumann
      source
      @[simp]
      theorem ZFSet.vonNeumann_inj {a b : Ordinal.{u}} :
      vonNeumann a = vonNeumann b ↔ a = b
      source
      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.

      source
      @[simp]
      theorem ZFSet.vonNeumann_zero :
      vonNeumann 0 = ∅
      source
      @[simp]
      theorem ZFSet.vonNeumann_succ (o : Ordinal.{u_1}) :
      vonNeumann (Order.succ o) = (vonNeumann o).powerset
      source
      theorem ZFSet.vonNeumann_of_isSuccPrelimit {o : Ordinal.{u}} (h : Order.IsSuccPrelimit o) :
      vonNeumann o = (range fun (a : ↑(Set.Iio o)) => vonNeumann ↑a).sUnion
      source
      theorem ZFSet.iUnion_vonNeumann :
      ⋃ (o : Ordinal.{u_1}), ↑(vonNeumann o) = Class.univ