Documentation

Mathlib.SetTheory.ZFC.Ordinal

Von Neumann ordinals #

This file works towards the development of von Neumann ordinals, i.e. transitive sets, well-ordered under . We currently only have an initial development of transitive sets.

Further development can be found on the branch von_neumann_v2.

Definitions #

Todo #

A transitive set is one where every element is a subset.

Equations
  • x.IsTransitive = yx, y x
Instances For
    @[simp]
    theorem ZFSet.empty_isTransitive :
    .IsTransitive
    theorem ZFSet.IsTransitive.subset_of_mem {x : ZFSet} {y : ZFSet} (h : x.IsTransitive) :
    y xy x
    theorem ZFSet.isTransitive_iff_mem_trans {z : ZFSet} :
    z.IsTransitive ∀ {x y : ZFSet}, x yy zx z
    theorem ZFSet.IsTransitive.mem_trans {z : ZFSet} :
    z.IsTransitive∀ {x y : ZFSet}, x yy zx z

    Alias of the forward direction of ZFSet.isTransitive_iff_mem_trans.

    theorem ZFSet.IsTransitive.inter {x : ZFSet} {y : ZFSet} (hx : x.IsTransitive) (hy : y.IsTransitive) :
    (x y).IsTransitive
    theorem ZFSet.IsTransitive.sUnion {x : ZFSet} (h : x.IsTransitive) :
    (⋃₀ x).IsTransitive
    theorem ZFSet.IsTransitive.sUnion' {x : ZFSet} (H : yx, y.IsTransitive) :
    (⋃₀ x).IsTransitive
    theorem ZFSet.IsTransitive.union {x : ZFSet} {y : ZFSet} (hx : x.IsTransitive) (hy : y.IsTransitive) :
    (x y).IsTransitive
    theorem ZFSet.IsTransitive.powerset {x : ZFSet} (h : x.IsTransitive) :
    x.powerset.IsTransitive
    theorem ZFSet.IsTransitive.sUnion_subset {x : ZFSet} :
    x.IsTransitive⋃₀ x x

    Alias of the forward direction of ZFSet.isTransitive_iff_sUnion_subset.

    theorem ZFSet.isTransitive_iff_subset_powerset {x : ZFSet} :
    x.IsTransitive x x.powerset
    theorem ZFSet.IsTransitive.subset_powerset {x : ZFSet} :
    x.IsTransitivex x.powerset

    Alias of the forward direction of ZFSet.isTransitive_iff_subset_powerset.