Class

📁 Source: Mathlib/SetTheory/ZFC/Class.lean

Statistics

Metric	Count
Definitions Class, ToSet, classToCong, congToClass, fval, instCoeZFSet, instMembership, instWellFoundedRelation, iota, ofSet, powerset, sInter, sUnion, sep, univ, «term_′_», «term⋂₀_», «term⋃₀_», choice, coeEquiv, toSet_equiv, instComplClass, instEmptyCollectionClass, instHasSubsetClass, instInsertZFSetClass, instInterClass, instNonemptyClass, instSDiffClass, instUnionClass	29
Theorems classToCong_empty, coe_apply, coe_diff, coe_empty, coe_insert, coe_inter, coe_mem, coe_powerset, coe_sInter, coe_sUnion, coe_sep, coe_subset, coe_union, congToClass_empty, eq_univ_iff_forall, eq_univ_of_forall, eq_univ_of_powerset_subset, ext, ext_iff, fval_ex, instIsWellFoundedMem, iota_ex, iota_val, mem_asymm, mem_def, mem_irrefl, mem_of_mem_sInter, mem_sInter, mem_sUnion, mem_univ, mem_univ_hom, mem_wf, notMem_empty, not_empty_hom, inj, powerset_apply, sInter_apply, sInter_empty, sUnion_apply, sUnion_empty, toSet_of_ZFSet, univ_notMem_univ, choice_isFunc, choice_mem, choice_mem_aux, coeEquiv_apply_coe, isOrdinal_notMem_univ, map_fval	48
Total	77

Class

Definitions

Name	Category	Theorems
ToSet 📖	MathDef	1 math math: toSet_of_ZFSet
classToCong 📖	CompOp	1 math math: classToCong_empty
congToClass 📖	CompOp	1 math math: congToClass_empty
fval 📖	CompOp	3 math math: fval_ex, ZFSet.choice_mem, ZFSet.map_fval
instCoeZFSet 📖	CompOp	—
instMembership 📖	CompOp	14 math math: iota_ex, notMem_empty, mem_univ, coe_mem, univ_notMem_univ, mem_sInter, ZFSet.isOrdinal_notMem_univ, mem_def, fval_ex, mem_irrefl, ZFSet.choice_mem, mem_sUnion, instIsWellFoundedMem, mem_wf
instWellFoundedRelation 📖	CompOp	—
iota 📖	CompOp	2 math math: iota_ex, iota_val
ofSet 📖	CompOp	20 math math: iota_val, mem_univ, coe_union, coe_insert, coe_mem, coe_sInter, coe_sUnion, coe_apply, coe_powerset, toSet_of_ZFSet, coe_subset, coe_sep, coe_diff, ZFSet.iUnion_vonNeumann, coe_empty, mem_def, coe_inter, ZFSet.choice_mem, powerset_apply, ZFSet.map_fval
powerset 📖	CompOp	2 math math: coe_powerset, powerset_apply
sInter 📖	CompOp	4 math math: coe_sInter, sInter_apply, mem_sInter, sInter_empty
sUnion 📖	CompOp	4 math math: sUnion_empty, coe_sUnion, mem_sUnion, sUnion_apply
sep 📖	CompOp	—
univ 📖	CompOp	11 math math: iota_ex, mem_univ, univ_notMem_univ, eq_univ_iff_forall, ZFSet.isOrdinal_notMem_univ, mem_univ_hom, eq_univ_of_forall, ZFSet.iUnion_vonNeumann, sInter_empty, fval_ex, eq_univ_of_powerset_subset
«term_′_» 📖	CompOp	—
«term⋂₀_» 📖	CompOp	—
«term⋃₀_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
classToCong_empty 📖	mathematical	—	classToCong Class instEmptyCollectionClass Set Set.instEmptyCollection	—	—
coe_apply 📖	mathematical	—	ofSet ZFSet ZFSet.instMembership	—	—
coe_diff 📖	mathematical	—	ofSet ZFSet ZFSet.instSDiff Class instSDiffClass	—	ext ZFSet.mem_sdiff
coe_empty 📖	mathematical	—	ofSet ZFSet ZFSet.instEmptyCollection Class instEmptyCollectionClass	—	ext ZFSet.notMem_empty
coe_insert 📖	mathematical	—	ofSet ZFSet ZFSet.instInsert Class instInsertZFSetClass	—	ext ZFSet.mem_insert_iff
coe_inter 📖	mathematical	—	ofSet ZFSet ZFSet.instInter Class instInterClass	—	ext ZFSet.mem_inter
coe_mem 📖	mathematical	—	Class instMembership ofSet	—	toSet_of_ZFSet
coe_powerset 📖	mathematical	—	ofSet ZFSet.powerset powerset	—	ext ZFSet.mem_powerset
coe_sInter 📖	mathematical	ZFSet.Nonempty	ofSet ZFSet.sInter sInter	—	Set.ext ZFSet.mem_sInter sInter_apply
coe_sUnion 📖	mathematical	—	ofSet ZFSet.sUnion sUnion	—	ext ZFSet.mem_sUnion sUnion_apply
coe_sep 📖	mathematical	—	ofSet ZFSet.sep setOf ZFSet ZFSet.instMembership	—	ext ZFSet.mem_sep
coe_subset 📖	mathematical	—	Class instHasSubsetClass ofSet ZFSet ZFSet.instHasSubset	—	—
coe_union 📖	mathematical	—	ofSet ZFSet ZFSet.instUnion Class instUnionClass	—	ext ZFSet.mem_union
congToClass_empty 📖	mathematical	—	congToClass Set Class Set.instEmptyCollection instEmptyCollectionClass	—	—
eq_univ_iff_forall 📖	mathematical	—	univ	—	Set.eq_univ_iff_forall
eq_univ_of_forall 📖	mathematical	—	univ	—	Set.eq_univ_of_forall
eq_univ_of_powerset_subset 📖	mathematical	Class instHasSubsetClass powerset	univ	—	eq_univ_of_forall WellFounded.min_mem ZFSet.mem_wf Mathlib.Tactic.Push.not_forall_eq WellFounded.not_lt_min coe_apply
ext 📖	—	—	—	—	Set.ext
ext_iff 📖	—	—	—	—	ext
fval_ex 📖	mathematical	—	Class instMembership univ fval	—	iota_ex
instIsWellFoundedMem 📖	mathematical	—	IsWellFounded Class instMembership	—	mem_wf
iota_ex 📖	mathematical	—	Class instMembership univ iota	—	mem_univ iota_val ext coe_empty
iota_val 📖	mathematical	—	iota ofSet	—	ext
mem_asymm 📖	—	Class instMembership	—	—	asymm_of instAsymmOfIsWellFounded instIsWellFoundedMem
mem_def 📖	mathematical	—	Class instMembership ofSet	—	—
mem_irrefl 📖	mathematical	—	Class instMembership	—	irrefl_of instAsymmOfIsWellFounded instIsWellFoundedMem
mem_of_mem_sInter 📖	—	Class instMembership sInter	—	—	coe_mem
mem_sInter 📖	mathematical	Set.Nonempty ZFSet	Class instMembership sInter	—	mem_of_mem_sInter coe_mem
mem_sUnion 📖	mathematical	—	Class instMembership sUnion	—	coe_mem
mem_univ 📖	mathematical	—	Class instMembership univ ofSet	—	—
mem_univ_hom 📖	mathematical	—	univ	—	—
mem_wf 📖	mathematical	—	Class instMembership	—	ZFSet.inductionOn
notMem_empty 📖	mathematical	—	Class instMembership instEmptyCollectionClass	—	—
not_empty_hom 📖	mathematical	—	Class instEmptyCollectionClass	—	—
powerset_apply 📖	mathematical	—	powerset Class instHasSubsetClass ofSet	—	—
sInter_apply 📖	mathematical	—	sInter ZFSet ZFSet.instMembership	—	—
sInter_empty 📖	mathematical	—	sInter Class instEmptyCollectionClass univ	—	sInter.eq_1 classToCong_empty Set.sInter_empty univ.eq_1
sUnion_apply 📖	mathematical	—	sUnion ZFSet ZFSet.instMembership	—	coe_mem
sUnion_empty 📖	mathematical	—	sUnion Class instEmptyCollectionClass	—	ext
toSet_of_ZFSet 📖	mathematical	—	ToSet ofSet	—	—
univ_notMem_univ 📖	mathematical	—	Class instMembership univ	—	mem_irrefl

Class.ofSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inj 📖	—	Class.ofSet	—	—	ZFSet.ext

ZFSet

Definitions

Name	Category	Theorems
choice 📖	CompOp	2 math math: choice_isFunc, choice_mem
coeEquiv 📖	CompOp	1 math math: coeEquiv_apply_coe
toSet_equiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
choice_isFunc 📖	mathematical	ZFSet instMembership instEmptyCollection	IsFunc sUnion choice	—	map_isFunc mem_sUnion choice_mem_aux
choice_mem 📖	mathematical	ZFSet instMembership instEmptyCollection	Class Class.instMembership Class.ofSet Class.fval choice	—	map_fval Class.coe_mem Class.coe_apply choice_mem_aux
choice_mem_aux 📖	mathematical	ZFSet instMembership instEmptyCollection	instInhabited	—	by_contradiction eq_empty
coeEquiv_apply_coe 📖	mathematical	—	Set ZFSet Small Set.Elem DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike coeEquiv SetLike.coe instSetLike	—	—
isOrdinal_notMem_univ 📖	mathematical	—	Class Class.instMembership Class.univ IsOrdinal	—	Class.coe_apply IsOrdinal.mem IsOrdinal.mem_trans Class.mem_irrefl Class.coe_mem
map_fval 📖	mathematical	ZFSet instMembership	Class.fval Class.ofSet map	—	Class.iota_val Class.toSet_of_ZFSet Class.coe_apply mem_map pair_injective

(root)

Definitions

Name	Category	Theorems
Class 📖	CompOp	26 math math: Class.iota_ex, Class.notMem_empty, Class.mem_univ, Class.coe_union, Class.coe_insert, Class.coe_mem, Class.sUnion_empty, Class.univ_notMem_univ, Class.congToClass_empty, Class.mem_sInter, Class.not_empty_hom, ZFSet.isOrdinal_notMem_univ, Class.coe_subset, Class.coe_diff, Class.sInter_empty, Class.coe_empty, Class.mem_def, Class.fval_ex, Class.mem_irrefl, Class.coe_inter, ZFSet.choice_mem, Class.powerset_apply, Class.mem_sUnion, Class.instIsWellFoundedMem, Class.classToCong_empty, Class.mem_wf
instComplClass 📖	CompOp	—
instEmptyCollectionClass 📖	CompOp	7 math math: Class.notMem_empty, Class.sUnion_empty, Class.congToClass_empty, Class.not_empty_hom, Class.sInter_empty, Class.coe_empty, Class.classToCong_empty
instHasSubsetClass 📖	CompOp	2 math math: Class.coe_subset, Class.powerset_apply
instInsertZFSetClass 📖	CompOp	1 math math: Class.coe_insert
instInterClass 📖	CompOp	1 math math: Class.coe_inter
instNonemptyClass 📖	CompOp	—
instSDiffClass 📖	CompOp	1 math math: Class.coe_diff
instUnionClass 📖	CompOp	1 math math: Class.coe_union

---

← Back to Index