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

Instances For

instance instClassHasSubset :

HasSubset Class.{u_1}

Equations

instance instClassEmptyCollection :

EmptyCollection Class.{u_1}

Equations

instance instClassNonempty :

Nonempty Class.{u_1}

Equations

instance instClassUnion :

Union Class.{u_1}

Equations

instance instClassInter :

Inter Class.{u_1}

Equations

instance instClassHasCompl :

HasCompl Class.{u_1}

Equations

instance instClassSDiff :

SDiff Class.{u_1}

Equations

instance instInsertZFSetClass :

Insert ZFSet.{u_1} Class.{u_1}

Equations

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

Instances For

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

Instances For

instance Class.instCoeZFSet :

Coe ZFSet.{u_1} Class.{u_1}

Equations

def Class.univ :

The universal class

Equations

Instances For

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

Assert that A is a ZFC set satisfying B

Equations

Instances For

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

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

Equations

Instances For

instance Class.instMembership :

Membership Class.{u_1} Class.{u_1}

Equations

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

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

Instances For

@[simp]

theorem Class.congToClass_empty :

congToClass ∅ = ∅

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

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

Equations

Instances For

@[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

Instances For

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

The union of a class is the class of all members of ZFC sets in the class. Uses ⋃₀ notation, scoped under the Class namespace.

Equations

Instances For

def Class.«term⋃₀_» :

Lean.ParserDescr

The union of a class is the class of all members of ZFC sets in the class. Uses ⋃₀ notation, scoped under the Class namespace.

Equations

Instances For

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

The intersection of a class is the class of all members of ZFC sets in the class . Uses ⋂₀ notation, scoped under the Class namespace.

Equations

Instances For

def Class.«term⋂₀_» :

Lean.ParserDescr

The intersection of a class is the class of all members of ZFC sets in the class . Uses ⋂₀ notation, scoped under the Class namespace.

Equations

Instances For

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.sUnion y ↔ ∃ (z : ZFSet.{u_1}), x z ∧ y ∈ z

@[simp]

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

↑x.sUnion = (↑x).sUnion

@[simp]

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

y ∈ x.sUnion ↔ ∃ z ∈ x, y ∈ z

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

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

@[simp]

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

↑x.sInter = (↑x).sInter

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

y ∈ z

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

y ∈ x.sInter ↔ ∀ z ∈ x, y ∈ z

@[simp]

theorem Class.sUnion_empty :

∅.sUnion = ∅

@[simp]

theorem Class.sInter_empty :

∅.sInter = 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

Instances For

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

Instances For

def Class.«term_′_» :

Lean.TrailingParserDescr

Function value

Equations

Instances For

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

Instances For

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

Instances For

@[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.