mathlib3 documentation

set_theory.zfc.ordinal

Von Neumann ordinals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 x y x
theorem Set.is_transitive_iff_mem_trans {z : Set} :
z.is_transitive {x y : Set}, x y y z x z
theorem Set.is_transitive.mem_trans {z : Set} :
z.is_transitive {x y : Set}, x y y z x 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]
@[protected]
theorem Set.is_transitive.union {x y : Set} (hx : x.is_transitive) (hy : y.is_transitive) :
@[protected]

Alias of the forward direction of Set.is_transitive_iff_sUnion_subset.