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 #

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

x.is_transitive = ∀ (y : Set), y ∈ x → y ⊆ x

@[simp]

theorem Set.empty_is_transitive :

∅.is_transitive

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) :

(x ∩ y).is_transitive

@[protected]

theorem Set.is_transitive.sUnion {x : Set} (h : x.is_transitive) :

(⋃₀ x).is_transitive

theorem Set.is_transitive.sUnion' {x : Set} (H : ∀ (y : Set), y ∈ x → y.is_transitive) :

(⋃₀ x).is_transitive

@[protected]

theorem Set.is_transitive.union {x y : Set} (hx : x.is_transitive) (hy : y.is_transitive) :

(x ∪ y).is_transitive

@[protected]

theorem Set.is_transitive.powerset {x : Set} (h : x.is_transitive) :

x.powerset.is_transitive

theorem Set.is_transitive_iff_sUnion_subset {x : Set} :

x.is_transitive ↔ ⋃₀ x ⊆ x

theorem Set.is_transitive.sUnion_subset {x : Set} :

x.is_transitive → ⋃₀ x ⊆ x

Alias of the forward direction of Set.is_transitive_iff_sUnion_subset.

theorem Set.is_transitive_iff_subset_powerset {x : Set} :

x.is_transitive ↔ x ⊆ x.powerset

theorem Set.is_transitive.subset_powerset {x : Set} :

x.is_transitive → x ⊆ x.powerset

Alias of the forward direction of Set.is_transitive_iff_subset_powerset.