| Metric | Count |
|---|
DefinitionsallZFSetDefinable, ZFSet, Definable, out, Definable₁, mk, out, Definable₂, mk, out, Hereditarily, IsFunc, diff, empty, funs, iUnion, image, instDefinable, instDefinableOfDefinable₁, instDefinableOfDefinable₂, instDefinable₁Singleton, instDefinable₂Insert, instDefinable₂Pair, instEmptyCollection, instHasSSubset, instHasSubset, instInhabited, instInsert, instInter, instMembership, instPartialOrder, instSDiff, instSep, instSetLike, instSingleton, instUnion, instWellFoundedRelation, inter, map, mk, omega, pair, pairSep, powerset, powersetEquiv, prod, range, sInter, sUnion, sep, toSet, union, «term⋂₀_», «term⋃_,_», «term⋃₀_» | 55 |
Theoremsmk_out, out_equiv, mk_out, out_equiv, mk_out, out_equiv, def, empty, mem, self, coe_empty, coe_iUnion, coe_image, coe_insert, coe_inter, coe_pair, coe_range, coe_sInter, coe_sUnion, coe_sdiff, coe_sep, coe_singleton, coe_subset_coe, coe_union, empty_subset, eq, eq_empty, eq_empty_or_nonempty, exact, ext, ext_iff, hereditarily_iff, mk, inductionOn, insert_eq, insert_nonempty, instAntisymmSubset, instIsNonstrictStrictOrderSubsetSSubset, instIsTransSubset, instIsWellFoundedMem, instLawfulSingleton, instReflSubset, inter_eq_left_of_subset, inter_eq_right_of_subset, le_def, lt_def, map_isFunc, map_unique, mem_asymm, mem_diff, mem_funs, mem_iUnion, mem_image, mem_insert, mem_insert_iff, mem_insert_of_mem, mem_inter, mem_irrefl, mem_map, mem_of_mem_sInter, mem_pair, mem_pairSep, mem_powerset, mem_prod, mem_range, mem_range_self, mem_sInter, mem_sUnion, mem_sUnion_of_mem, mem_sdiff, mem_sep, mem_singleton, mem_toSet, mem_union, mem_wf, mk_eq, mk_mem_iff, mk_out, nonempty_coe, nonempty_def, nonempty_mk_iff, nonempty_of_mem, nonempty_toSet_iff, notMem_empty, notMem_of_subset, notMem_sInter_of_notMem, notMem_singleton, not_nonempty_empty, not_subset_of_mem, omega_succ, omega_zero, pair_eq_singleton, pair_eq_singleton_iff, pair_inj, pair_injective, pair_mem_prod, regularity, sInter_empty, sInter_singleton, sUnion_empty, sUnion_lem, sUnion_pair, sUnion_singleton, sep_empty, sep_mem, sep_notMem, sep_subset, singleton_eq_pair_iff, singleton_inj, singleton_injective, singleton_nonempty, small_coe, small_toSet, sound, subset_def, subset_iUnion, subset_iff, toSet_empty, toSet_iUnion, toSet_image, toSet_inj, toSet_injective, toSet_insert, toSet_inter, toSet_pair, toSet_range, toSet_sInter, toSet_sUnion, toSet_sdiff, toSet_sep, toSet_singleton, toSet_subset_iff, toSet_union | 133 |
| Total | 188 |
| Name | Category | Theorems |
|---|
Definable 📖 | CompData | — |
Definable₁ 📖 | CompOp | — |
Definable₂ 📖 | CompOp | — |
Hereditarily 📖 | MathDef | 1 mathmath: hereditarily_iff
|
IsFunc 📖 | MathDef | 3 mathmath: choice_isFunc, map_isFunc, mem_funs
|
diff 📖 | CompOp | — |
empty 📖 | CompOp | — |
funs 📖 | CompOp | 1 mathmath: mem_funs
|
iUnion 📖 | CompOp | 9 mathmath: mem_iUnion, lift_card_iUnion_le_sum_card, coe_iUnion, IsTransitive.iUnion, rank_iUnion, toSet_iUnion, vonNeumann_of_isSuccPrelimit, subset_iUnion, iSup_card_le_card_iUnion
|
image 📖 | CompOp | 5 mathmath: coe_image, toSet_image, mem_image, image.mk, card_image_le
|
instDefinable 📖 | CompOp | — |
instDefinableOfDefinable₁ 📖 | CompOp | — |
instDefinableOfDefinable₂ 📖 | CompOp | — |
instDefinable₁Singleton 📖 | CompOp | — |
instDefinable₂Insert 📖 | CompOp | — |
instDefinable₂Pair 📖 | CompOp | — |
instEmptyCollection 📖 | CompOp | 21 mathmath: rank_empty, notMem_empty, eq_empty, isOrdinal_empty, toSet_empty, Hereditarily.empty, empty_subset, regularity, eq_empty_or_nonempty, vonNeumann_zero, Class.coe_empty, sInter_empty, isTransitive_empty, sep_empty, coe_empty, instLawfulSingleton, card_empty, not_nonempty_empty, Ordinal.toZFSet_zero, sUnion_empty, omega_zero
|
instHasSSubset 📖 | CompOp | 2 mathmath: instIsNonstrictStrictOrderSubsetSSubset, lt_def
|
instHasSubset 📖 | CompOp | 34 mathmath: instAntisymmSubset, IsOrdinal.rank_le_iff_subset, subset_vonNeumann, vonNeumann_subset_vonNeumann_iff, subset_def, IsTransitive.subset_of_mem, vonNeumann_subset_of_le, mem_powerset, instIsNonstrictStrictOrderSubsetSSubset, empty_subset, coe_subset_coe, mem_vonNeumann', not_subset_of_mem, IsOrdinal.notMem_iff_subset, Class.coe_subset, subset_vonNeumann_self, instReflSubset, subset_iff, IsOrdinal.subset_of_mem, IsOrdinal.mem_or_subset, toSet_subset_iff, Ordinal.toZFSet_subset_vonNeumann, isTransitive_iff_subset_powerset, Ordinal.toZFSet_subset_toZFSet_iff, IsTransitive.sUnion_subset, IsTransitive.subset_powerset, le_def, IsOrdinal.subset_total, instIsTransSubset, IsOrdinal.subset_iff_eq_or_mem, sep_subset, subset_iUnion, isTransitive_iff_sUnion_subset, IsOrdinal.not_subset_iff_mem
|
instInhabited 📖 | CompOp | 1 mathmath: choice_mem_aux
|
instInsert 📖 | CompOp | 24 mathmath: Class.coe_insert, coe_pair, coe_insert, mem_insert_of_mem, sUnion_pair, pair_eq_singleton_iff, pair_eq_singleton, card_pair_of_ne, isOrdinal_succ, singleton_eq_pair_iff, insert_nonempty, mem_pair, insert_eq, toSet_pair, rank_insert, card_insert_le, card_insert, toSet_insert, instLawfulSingleton, mem_insert_iff, rank_pair, Ordinal.toZFSet_succ, omega_succ, mem_insert
|
instInter 📖 | CompOp | 9 mathmath: coe_inter, sep_mem, mem_inter, inter_eq_left_of_subset, regularity, toSet_inter, Class.coe_inter, IsTransitive.inter, inter_eq_right_of_subset
|
instMembership 📖 | CompOp | 70 mathmath: sep_notMem, mem_toSet, lt_rank_iff, mem_sep, notMem_empty, eq_empty, sep_mem, subset_def, IsOrdinal.trichotomous, notMem_singleton, pair_mem_prod, nonempty_def, mem_powerset, mem_inter, mem_iUnion, Class.sInter_apply, exists_mem_vonNeumann, Ordinal.mem_toZFSet_iff, map_isFunc, Class.coe_apply, mem_sUnion, mem_pairSep, mem_vonNeumann', vonNeumann_mem_vonNeumann_iff, coe_sep, IsOrdinal.notMem_iff_subset, IsOrdinal.eq_or_mem_of_subset, regularity, IsOrdinal.isTrichotomous, Class.coe_sep, IsOrdinal.isTrans, mem_wf, IsOrdinal.isWellOrder, instIsWellFoundedMem, mem_pair, mem_funs, mk_mem_iff, toSet_sep, mem_prod, mem_irrefl, mem_sdiff, isOrdinal_iff_isTrans, IsOrdinal.mem_or_subset, isOrdinal_iff_isTrichotomous, isOrdinal_iff_trichotomous, mem_vonNeumann_succ, mem_vonNeumann, notMem_of_subset, mem_image, IsOrdinal.mem_trichotomous, rank_eq_wfRank, isOrdinal_iff_isWellOrder, ext_iff, mem_insert_iff, isTransitive_iff_mem_trans, mem_singleton, mem_map, mem_diff, mem_range, vonNeumann_mem_of_lt, IsOrdinal.rank_lt_iff_mem, IsOrdinal.subset_iff_eq_or_mem, omega_zero, Ordinal.toZFSet_mem_toZFSet_iff, mem_range_self, mem_sInter, Class.sUnion_apply, mem_union, mem_insert, IsOrdinal.not_subset_iff_mem
|
instPartialOrder 📖 | CompOp | 7 mathmath: Ordinal.toZFSet_strictMono, vonNeumann_strictMono, Ordinal.toZFSetIso_apply, le_def, Ordinal.toZFSet_monotone, lt_def, Ordinal.toZFSetIso_symm_apply
|
instSDiff 📖 | CompOp | 6 mathmath: sep_notMem, Class.coe_diff, coe_sdiff, mem_sdiff, toSet_sdiff, mem_diff
|
instSep 📖 | CompOp | — |
instSetLike 📖 | CompOp | 38 mathmath: coe_inter, coe_image, mem_toSet, coe_pair, coe_insert, toSet_empty, Ordinal.coe_toZFSet, coe_singleton, coeEquiv_apply_coe, toSet_image, coe_range, toSet_inj, coe_subset_coe, coe_sUnion, coe_sep, coe_iUnion, coe_sdiff, toSet_pair, toSet_sep, toSet_injective, toSet_subset_iff, toSet_insert, nonempty_coe, toSet_sInter, coe_empty, toSet_singleton, nonempty_toSet_iff, coe_sInter, toSet_sdiff, toSet_inter, cardinalMk_coe_sort, small_toSet, toSet_iUnion, toSet_sUnion, toSet_range, small_coe, toSet_union, coe_union
|
instSingleton 📖 | CompOp | 22 mathmath: sInter_singleton, coe_pair, sUnion_singleton, card_singleton, singleton_nonempty, sUnion_pair, notMem_singleton, coe_singleton, pair_eq_singleton_iff, pair_eq_singleton, card_pair_of_ne, singleton_eq_pair_iff, mem_pair, insert_eq, toSet_pair, singleton_injective, toSet_singleton, instLawfulSingleton, mem_singleton, singleton_inj, rank_pair, rank_singleton
|
instUnion 📖 | CompOp | 9 mathmath: Class.coe_union, sUnion_pair, insert_eq, card_union_le, IsTransitive.union, rank_union, mem_union, toSet_union, coe_union
|
instWellFoundedRelation 📖 | CompOp | — |
inter 📖 | CompOp | — |
map 📖 | CompOp | 4 mathmath: map_isFunc, map_unique, mem_map, map_fval
|
mk 📖 | CompOp | — |
omega 📖 | CompOp | 1 mathmath: omega_zero
|
pair 📖 | CompOp | 9 mathmath: coe_pair, pair_mem_prod, pair_injective, mem_pairSep, map_unique, toSet_pair, mem_prod, pair_inj, mem_map
|
pairSep 📖 | CompOp | 1 mathmath: mem_pairSep
|
powerset 📖 | CompOp | 8 mathmath: mem_powerset, Class.coe_powerset, rank_powerset, IsTransitive.powerset, isTransitive_iff_subset_powerset, IsTransitive.subset_powerset, card_powerset, vonNeumann_succ
|
powersetEquiv 📖 | CompOp | — |
prod 📖 | CompOp | 2 mathmath: pair_mem_prod, mem_prod
|
range 📖 | CompOp | 6 mathmath: coe_range, lift_card_range_le, rank_range, mem_range, toSet_range, mem_range_self
|
sInter 📖 | CompOp | 7 mathmath: sInter_singleton, Class.coe_sInter, sInter_empty, toSet_sInter, coe_sInter, notMem_sInter_of_notMem, mem_sInter
|
sUnion 📖 | CompOp | 15 mathmath: IsTransitive.sUnion', mem_sUnion_of_mem, sUnion_singleton, sUnion_pair, choice_isFunc, Class.coe_sUnion, mem_sUnion, coe_sUnion, rank_sUnion_le, IsTransitive.sUnion_subset, IsTransitive.sUnion, sUnion_empty, toSet_sUnion, le_succ_rank_sUnion, isTransitive_iff_sUnion_subset
|
sep 📖 | CompOp | 8 mathmath: sep_notMem, mem_sep, sep_mem, coe_sep, Class.coe_sep, toSet_sep, sep_empty, sep_subset
|
toSet 📖 | CompOp | — |
union 📖 | CompOp | — |
«term⋂₀_» 📖 | CompOp | — |
«term⋃_,_» 📖 | CompOp | — |
«term⋃₀_» 📖 | CompOp | — |