Documentation

Mathlib.SetTheory.ZFC.Class

ZFC classes #

Classes in set theory are usually defined as collections of elements satisfying some property. Here, however, we define Class as Set ZFSet to derive many instances automatically, most of them being the lifting of set operations to classes. The usual definition is then definitionally equal to ours.

Main definitions #

Class: Defined as Set ZFSet.
Class.iota: Definite description operator.
ZFSet.isOrdinal_notMem_univ: The Burali-Forti paradox. Ordinals form a proper class.

def Class :

Type (u_1 + 1)

The collection of all classes. We define Class as Set ZFSet, as this allows us to get many instances automatically. However, in practice, we treat it as (the definitionally equal) ZFSet → Prop. This means, the preferred way to state that x : ZFSet belongs to A : Class is to write A x.

Equations

Class.{?u.2} = Set ZFSet.{?u.2}

instance instClassHasSubset :

HasSubset Class.{u_1}

Equations

instClassHasSubset = Set.instHasSubset

instance instClassEmptyCollection :

EmptyCollection Class.{u_1}

Equations

instClassEmptyCollection = Set.instEmptyCollection

instance instClassNonempty :

Nonempty Class.{u_1}

Equations

instClassNonempty = ⋯

instance instClassUnion :

Union Class.{u_1}

Equations

instClassUnion = Set.instUnion

instance instClassInter :

Inter Class.{u_1}

Equations

instClassInter = Set.instInter

instance instClassHasCompl :

HasCompl Class.{u_1}

Equations

instClassHasCompl = Set.instHasCompl

instance instClassSDiff :

SDiff Class.{u_1}

Equations

instClassSDiff = Set.instSDiff

instance instInsertZFSetClass :

Insert ZFSet.{u_1} Class.{u_1}

Equations

instInsertZFSetClass = { insert := Set.insert }

def Class.sep (p : ZFSet.{u_1} → Prop) (A : Class.{u_1}) :

{x ∈ A | p x} is the class of elements in A satisfying p

Equations

Class.sep p A = {y : ZFSet.{?u.12} | A y ∧ p y}

theorem Class.ext {x y : Class.{u}} :

(∀ (z : ZFSet.{u}), x z ↔ y z) → x = y

theorem Class.ext_iff {x y : Class.{u}} :

x = y ↔ ∀ (z : ZFSet.{u}), x z ↔ y z

def Class.ofSet (x : ZFSet.{u}) :

Coerce a ZFC set into a class

Equations

↑x = {y : ZFSet.{?u.7} | y ∈ x}

instance Class.instCoeZFSet :

Coe ZFSet.{u_1} Class.{u_1}

Equations

Class.instCoeZFSet = { coe := Class.ofSet }

def Class.univ :

The universal class

Equations

Class.univ = Set.univ

def Class.ToSet (B A : Class.{u}) :

Assert that A is a ZFC set satisfying B

Equations

B.ToSet A = ∃ (x : ZFSet.{?u.11}), ↑x = A ∧ B x

def Class.Mem (B A : Class.{u}) :

A ∈ B if A is a ZFC set which satisfies B

Equations

B.Mem A = B.ToSet A

instance Class.instMembership :

Membership Class.{u_1} Class.{u_1}

Equations

Class.instMembership = { mem := Class.Mem }

theorem Class.mem_def (A B : Class.{u}) :

A ∈ B ↔ ∃ (x : ZFSet.{u}), ↑x = A ∧ B x

@[simp]

theorem Class.notMem_empty (x : Class.{u}) :

x ∉ ∅

@[deprecated Class.notMem_empty (since := "2025-05-23")]

theorem Class.not_mem_empty (x : Class.{u}) :

x ∉ ∅

Alias of Class.notMem_empty.

@[simp]

theorem Class.not_empty_hom (x : ZFSet.{u}) :

@[simp]

theorem Class.mem_univ {A : Class.{u}} :

A ∈ univ ↔ ∃ (x : ZFSet.{u}), ↑x = A

@[simp]

theorem Class.mem_univ_hom (x : ZFSet.{u}) :

theorem Class.eq_univ_iff_forall {A : Class.{u}} :

A = univ ↔ ∀ (x : ZFSet.{u}), A x

theorem Class.eq_univ_of_forall {A : Class.{u}} :

(∀ (x : ZFSet.{u}), A x) → A = univ

theorem Class.mem_wf :

WellFounded fun (x1 x2 : Class.{u}) => x1 ∈ x2

instance Class.instIsWellFoundedMem :

IsWellFounded Class.{u_1} fun (x1 x2 : Class.{u_1}) => x1 ∈ x2

instance Class.instWellFoundedRelation :

WellFoundedRelation Class.{u_1}

Equations

Class.instWellFoundedRelation = { rel := fun (x1 x2 : Class.{?u.4}) => x1 ∈ x2, wf := Class.mem_wf }

theorem Class.mem_asymm {x y : Class.{u_1}} :

x ∈ y → y ∉ x

theorem Class.mem_irrefl (x : Class.{u_1}) :

x ∉ x

theorem Class.univ_notMem_univ :

There is no universal set. This is stated as univ ∉ univ, meaning that univ (the class of all sets) is proper (does not belong to the class of all sets).

@[deprecated Class.univ_notMem_univ (since := "2025-05-23")]

theorem Class.univ_not_mem_univ :

Alias of Class.univ_notMem_univ.

There is no universal set. This is stated as univ ∉ univ, meaning that univ (the class of all sets) is proper (does not belong to the class of all sets).

def Class.congToClass (x : Set Class.{u}) :

Convert a conglomerate (a collection of classes) into a class

Equations

Class.congToClass x = {y : ZFSet.{?u.2} | ↑y ∈ x}

@[simp]

theorem Class.congToClass_empty :

congToClass ∅ = ∅

def Class.classToCong (x : Class.{u}) :

Convert a class into a conglomerate (a collection of classes)

Equations

x.classToCong = {y : Class.{?u.2} | y ∈ x}

@[simp]

theorem Class.classToCong_empty :

∅.classToCong = ∅

def Class.powerset (x : Class.{u_1}) :

The power class of a class is the class of all subclasses that are ZFC sets

Equations

x.powerset = Class.congToClass (𝒫 x)

def Class.sUnion (x : Class.{u_1}) :

The union of a class is the class of all members of ZFC sets in the class

Equations

⋃₀ x = ⋃₀ x.classToCong

def Class.«term⋃₀_» :

Lean.ParserDescr

The union of a class is the class of all members of ZFC sets in the class

Equations

Class.«term⋃₀_» = Lean.ParserDescr.node `Class.«term⋃₀_» 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋃₀ ") (Lean.ParserDescr.cat `term 110))

def Class.sInter (x : Class.{u_1}) :

The intersection of a class is the class of all members of ZFC sets in the class

Equations

⋂₀ x = ⋂₀ x.classToCong

def Class.«term⋂₀_» :

Lean.ParserDescr

The intersection of a class is the class of all members of ZFC sets in the class

Equations

Class.«term⋂₀_» = Lean.ParserDescr.node `Class.«term⋂₀_» 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋂₀ ") (Lean.ParserDescr.cat `term 110))

theorem Class.ofSet.inj {x y : ZFSet.{u}} (h : ↑x = ↑y) :

x = y

@[simp]

theorem Class.toSet_of_ZFSet (A : Class.{u}) (x : ZFSet.{u}) :

A.ToSet ↑x ↔ A x

@[simp]

theorem Class.coe_mem {x : ZFSet.{u}} {A : Class.{u}} :

↑x ∈ A ↔ A x

@[simp]

theorem Class.coe_apply {x y : ZFSet.{u}} :

↑y x ↔ x ∈ y

@[simp]

theorem Class.coe_subset (x y : ZFSet.{u}) :

↑x ⊆ ↑y ↔ x ⊆ y

@[simp]

theorem Class.coe_sep (p : Class.{u}) (x : ZFSet.{u}) :

↑(ZFSet.sep p x) = {y : ZFSet.{u} | y ∈ x ∧ p y}

@[simp]

theorem Class.coe_empty :

@[simp]

theorem Class.coe_insert (x y : ZFSet.{u}) :

↑(insert x y) = insert x ↑y

@[simp]

theorem Class.coe_union (x y : ZFSet.{u}) :

↑(x ∪ y) = ↑x ∪ ↑y

@[simp]

theorem Class.coe_inter (x y : ZFSet.{u}) :

↑(x ∩ y) = ↑x ∩ ↑y

@[simp]

theorem Class.coe_diff (x y : ZFSet.{u}) :

↑(x \ y) = ↑x \ ↑y

@[simp]

theorem Class.coe_powerset (x : ZFSet.{u}) :

↑x.powerset = (↑x).powerset

@[simp]

theorem Class.powerset_apply {A : Class.{u}} {x : ZFSet.{u}} :

A.powerset x ↔ ↑x ⊆ A

@[simp]

theorem Class.sUnion_apply {x : Class.{u_1}} {y : ZFSet.{u_1}} :

(⋃₀ x) y ↔ ∃ (z : ZFSet.{u_1}), x z ∧ y ∈ z

@[simp]

theorem Class.coe_sUnion (x : ZFSet.{u}) :

↑(⋃₀ x) = ⋃₀ ↑x

@[simp]

theorem Class.mem_sUnion {x y : Class.{u}} :

y ∈ ⋃₀ x ↔ ∃ z ∈ x, y ∈ z

theorem Class.sInter_apply {x : Class.{u}} {y : ZFSet.{u}} :

(⋂₀ x) y ↔ ∀ (z : ZFSet.{u}), x z → y ∈ z

@[simp]

theorem Class.coe_sInter {x : ZFSet.{u}} (h : x.Nonempty) :

↑(⋂₀ x) = ⋂₀ ↑x

theorem Class.mem_of_mem_sInter {x y z : Class.{u_1}} (hy : y ∈ ⋂₀ x) (hz : z ∈ x) :

y ∈ z

theorem Class.mem_sInter {x y : Class.{u}} (h : Set.Nonempty x) :

y ∈ ⋂₀ x ↔ ∀ z ∈ x, y ∈ z

@[simp]

theorem Class.sUnion_empty :

⋃₀ ∅ = ∅

@[simp]

theorem Class.sInter_empty :

⋂₀ ∅ = univ

theorem Class.eq_univ_of_powerset_subset {A : Class.{u_1}} (hA : A.powerset ⊆ A) :

An induction principle for sets. If every subset of a class is a member, then the class is universal.

def Class.iota (A : Class.{u_1}) :

The definite description operator, which is {x} if {y | A y} = {x} and ∅ otherwise.

Equations

A.iota = ⋃₀ {x : ZFSet.{?u.8} | ∀ (y : ZFSet.{?u.8}), A y ↔ y = x}

theorem Class.iota_val (A : Class.{u_1}) (x : ZFSet.{u_1}) (H : ∀ (y : ZFSet.{u_1}), A y ↔ y = x) :

A.iota = ↑x

theorem Class.iota_ex (A : Class.{u}) :

A.iota ∈ univ

Unlike the other set constructors, the iota definite descriptor is a set for any set input, but not constructively so, so there is no associated Class → Set function.

def Class.fval (F A : Class.{u}) :

Function value

Equations

F ′ A = Class.iota fun (y : ZFSet.{?u.12}) => Class.ToSet (fun (x : ZFSet.{?u.12}) => F (x.pair y)) A

def Class.«term_′_» :

Lean.TrailingParserDescr

Function value

Equations

Class.«term_′_» = Lean.ParserDescr.trailingNode `Class.«term_′_» 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ′ ") (Lean.ParserDescr.cat `term 101))

theorem Class.fval_ex (F A : Class.{u}) :

F ′ A ∈ univ

@[simp]

theorem ZFSet.map_fval {f : ZFSet.{u} → ZFSet.{u}} [Definable₁ f] {x y : ZFSet.{u}} (h : y ∈ x) :

↑(map f x) ′ ↑y = ↑(f y)

noncomputable def ZFSet.choice (x : ZFSet.{u}) :

A choice function on the class of nonempty ZFC sets.

Equations

x.choice = ZFSet.map (fun (y : ZFSet.{?u.10}) => Classical.epsilon fun (z : ZFSet.{?u.10}) => z ∈ y) x

theorem ZFSet.choice_mem_aux (x : ZFSet.{u}) (h : ∅ ∉ x) (y : ZFSet.{u}) (yx : y ∈ x) :

(Classical.epsilon fun (z : ZFSet.{u}) => z ∈ y) ∈ y

theorem ZFSet.choice_isFunc (x : ZFSet.{u}) (h : ∅ ∉ x) :

x.IsFunc (⋃₀ x) x.choice

theorem ZFSet.choice_mem (x : ZFSet.{u}) (h : ∅ ∉ x) (y : ZFSet.{u}) (yx : y ∈ x) :

↑x.choice ′ ↑y ∈ ↑y

noncomputable def ZFSet.toSet_equiv :

ZFSet.{u} ≃ { s : Set ZFSet.{u} // Small.{u, u + 1} ↑s }

ZFSet.toSet as an equivalence.

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem ZFSet.toSet_equiv_apply_coe (x : ZFSet.{u}) :

↑(toSet_equiv x) = x.toSet

theorem ZFSet.isOrdinal_notMem_univ :

IsOrdinal ∉ Class.univ

The Burali-Forti paradox: ordinals form a proper class.

@[deprecated ZFSet.isOrdinal_notMem_univ (since := "2025-05-23")]

theorem ZFSet.isOrdinal_not_mem_univ :

IsOrdinal ∉ Class.univ

Alias of ZFSet.isOrdinal_notMem_univ.

The Burali-Forti paradox: ordinals form a proper class.