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.

def ZFSet.IsTransitive (x : ZFSet) :

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

Equations

ZFSet.IsTransitive x = ∀ y ∈ x, y ⊆ x

Instances For

@[simp]

theorem ZFSet.empty_isTransitive :

ZFSet.IsTransitive ∅

theorem ZFSet.IsTransitive.subset_of_mem {x : ZFSet} {y : ZFSet} (h : ZFSet.IsTransitive x) :

y ∈ x → y ⊆ x

theorem ZFSet.isTransitive_iff_mem_trans {z : ZFSet} :

ZFSet.IsTransitive z ↔ ∀ {x y : ZFSet}, x ∈ y → y ∈ z → x ∈ z

theorem ZFSet.IsTransitive.mem_trans {z : ZFSet} :

ZFSet.IsTransitive z → ∀ {x y : ZFSet}, x ∈ y → y ∈ z → x ∈ z

Alias of the forward direction of ZFSet.isTransitive_iff_mem_trans.

theorem ZFSet.IsTransitive.inter {x : ZFSet} {y : ZFSet} (hx : ZFSet.IsTransitive x) (hy : ZFSet.IsTransitive y) :

ZFSet.IsTransitive (x ∩ y)

theorem ZFSet.IsTransitive.sUnion {x : ZFSet} (h : ZFSet.IsTransitive x) :

ZFSet.IsTransitive (⋃₀ x)

theorem ZFSet.IsTransitive.sUnion' {x : ZFSet} (H : ∀ y ∈ x, ZFSet.IsTransitive y) :

ZFSet.IsTransitive (⋃₀ x)

theorem ZFSet.IsTransitive.union {x : ZFSet} {y : ZFSet} (hx : ZFSet.IsTransitive x) (hy : ZFSet.IsTransitive y) :

ZFSet.IsTransitive (x ∪ y)

theorem ZFSet.IsTransitive.powerset {x : ZFSet} (h : ZFSet.IsTransitive x) :

ZFSet.IsTransitive (ZFSet.powerset x)

theorem ZFSet.isTransitive_iff_sUnion_subset {x : ZFSet} :

ZFSet.IsTransitive x ↔ ⋃₀ x ⊆ x

theorem ZFSet.IsTransitive.sUnion_subset {x : ZFSet} :

ZFSet.IsTransitive x → ⋃₀ x ⊆ x

Alias of the forward direction of ZFSet.isTransitive_iff_sUnion_subset.

theorem ZFSet.isTransitive_iff_subset_powerset {x : ZFSet} :

ZFSet.IsTransitive x ↔ x ⊆ ZFSet.powerset x

theorem ZFSet.IsTransitive.subset_powerset {x : ZFSet} :

ZFSet.IsTransitive x → x ⊆ ZFSet.powerset x

Alias of the forward direction of ZFSet.isTransitive_iff_subset_powerset.