# 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 #

• ZFSet.IsTransitive means that every element of a set is a subset.

## Todo #

• Define von Neumann ordinals.
• Define the basic arithmetic operations on ordinals from a purely set-theoretic perspective.
• Prove the equivalences between these definitions and those provided in SetTheory/Ordinal/Arithmetic.lean.

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.