Cocardinal

📁 Source: Mathlib/Order/Filter/Cocardinal.lean

Statistics

Metric	Count
Definitions cocardinal, cocountable	2
Theorems cocardinal_aleph0_eq_cofinite, cocardinal_inf_principal_neBot_iff, compl_mem_cocardinal_of_card_lt, eventually_cocardinal, eventually_cocardinal_ne, eventually_cocardinal_notMem_of_card_lt, frequently_cocardinal, frequently_cocardinal_mem, hasBasis_cocardinal, instCardinalInterFilter_cocardinal, mem_cocardinal, mem_cocountable, eventually_cocardinal_notMem, compl_mem_cocardinal	14
Total	16

Filter

Definitions

Name	Category	Theorems
cocardinal 📖	CompOp	13 math math: instCardinalInterFilter_cocardinal, compl_mem_cocardinal_of_card_lt, mem_cocardinal, frequently_cocardinal, eventually_cocardinal_ne, cocardinal_aleph0_eq_cofinite, hasBasis_cocardinal, eventually_cocardinal, eventually_cocardinal_notMem_of_card_lt, cocardinal_inf_principal_neBot_iff, frequently_cocardinal_mem, Set.Finite.compl_mem_cocardinal, Finset.eventually_cocardinal_notMem
cocountable 📖	CompOp	1 math math: mem_cocountable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cocardinal_aleph0_eq_cofinite 📖	mathematical	—	cocardinal Cardinal.aleph0 Cardinal.isRegular_aleph0 cofinite	—	ext Cardinal.isRegular_aleph0
cocardinal_inf_principal_neBot_iff 📖	mathematical	Cardinal.IsRegular	NeBot Filter instInf cocardinal principal Cardinal Cardinal.instLE Set.Elem	—	frequently_mem_iff_neBot frequently_cocardinal
compl_mem_cocardinal_of_card_lt 📖	mathematical	Cardinal.IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Set.Elem	Set Filter instMembership cocardinal Compl.compl Set.instCompl	—	mem_cocardinal compl_compl
eventually_cocardinal 📖	mathematical	Cardinal.IsRegular	Eventually cocardinal Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Set.Elem setOf	—	—
eventually_cocardinal_ne 📖	mathematical	Cardinal.IsRegular	Eventually cocardinal	—	Cardinal.mk_fintype Fintype.card_unique Nat.cast_one Cardinal.IsRegular.nat_lt
eventually_cocardinal_notMem_of_card_lt 📖	mathematical	Cardinal.IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Set.Elem	Eventually Set Set.instMembership cocardinal	—	compl_mem_cocardinal_of_card_lt
frequently_cocardinal 📖	mathematical	Cardinal.IsRegular	Frequently cocardinal Cardinal Cardinal.instLE Set.Elem setOf	—	—
frequently_cocardinal_mem 📖	mathematical	Cardinal.IsRegular	Frequently Set Set.instMembership cocardinal Cardinal Cardinal.instLE Set.Elem	—	frequently_cocardinal
hasBasis_cocardinal 📖	mathematical	Cardinal.IsRegular	HasBasis Set cocardinal setOf Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Set.Elem Compl.compl Set.instCompl	—	Eq.subset Set.instReflSubset compl_compl lt_of_le_of_lt Cardinal.mk_le_mk_of_subset Set.compl_subset_comm
instCardinalInterFilter_cocardinal 📖	mathematical	Cardinal.IsRegular	CardinalInterFilter cocardinal	—	mem_cocardinal Set.compl_sInter lt_of_le_of_lt Cardinal.mk_sUnion_le Cardinal.mul_lt_of_lt Cardinal.IsRegular.aleph0_le Cardinal.mk_image_le Cardinal.iSup_lt_of_isRegular
mem_cocardinal 📖	mathematical	Cardinal.IsRegular	Set Filter instMembership cocardinal Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Set.Elem Compl.compl Set.instCompl	—	—
mem_cocountable 📖	mathematical	—	Set Filter instMembership cocountable Set.Countable Compl.compl Set.instCompl	—	Cardinal.countable_iff_lt_aleph_one Cardinal.isRegular_aleph_one mem_cocardinal

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eventually_cocardinal_notMem 📖	mathematical	Cardinal.IsRegular	Filter.Eventually Finset instMembership Filter.cocardinal	—	Filter.eventually_cocardinal_notMem_of_card_lt LT.lt.trans_le Cardinal.finset_card_lt_aleph0 Cardinal.IsRegular.aleph0_le

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compl_mem_cocardinal 📖	mathematical	Cardinal.IsRegular	Set Filter Filter.instMembership Filter.cocardinal Compl.compl Set.instCompl	—	Filter.compl_mem_cocardinal_of_card_lt lt_of_lt_of_le lt_aleph0 Cardinal.IsRegular.aleph0_le

---

← Back to Index