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

• 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.

Instances For
@[simp]
theorem ZFSet.IsTransitive.subset_of_mem {x : ZFSet} {y : ZFSet} (h : ) :
y xy x
theorem ZFSet.isTransitive_iff_mem_trans {z : ZFSet} :
∀ {x y : ZFSet}, x yy zx z
theorem ZFSet.IsTransitive.mem_trans {z : ZFSet} :
∀ {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 : ) (hy : ) :
theorem ZFSet.IsTransitive.sUnion {x : ZFSet} (h : ) :
theorem ZFSet.IsTransitive.sUnion' {x : ZFSet} (H : ∀ (y : ZFSet), y x) :
theorem ZFSet.IsTransitive.union {x : ZFSet} {y : ZFSet} (hx : ) (hy : ) :

Alias of the forward direction of ZFSet.isTransitive_iff_sUnion_subset.

Alias of the forward direction of ZFSet.isTransitive_iff_subset_powerset.