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