mathlib documentation

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 #

Todo #

def Set.is_transitive (x : Set) :
Prop

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

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