# mathlibdocumentation

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

• Set.is_transitive 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 set_theory/ordinal/arithmetic.lean.
def Set.is_transitive (x : Set) :
Prop

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

Equations
@[simp]
theorem Set.is_transitive.subset_of_mem {x y : Set} (h : x.is_transitive) :
y xy x
theorem Set.is_transitive_iff_mem_trans {z : Set} :
z.is_transitive ∀ {x y : Set}, x yy zx z
theorem Set.is_transitive.mem_trans {z : Set} :
z.is_transitive∀ {x y : Set}, x yy zx z

Alias of the forward direction of Set.is_transitive_iff_mem_trans.

@[protected]
theorem Set.is_transitive.inter {x y : Set} (hx : x.is_transitive) (hy : y.is_transitive) :
@[protected]
theorem Set.is_transitive.sUnion' {x : Set} (H : ∀ (y : Set), y x → y.is_transitive) :

Alias of the forward direction of Set.is_transitive_iff_sUnion_subset.

Alias of the forward direction of Set.is_transitive_iff_subset_powerset.