Commit 2023-02-24 13:27 6c36fbf6

View on Github →

feat port: SetTheory.Cardinal.Cofinality (#2479)

Estimated changes

Modified Mathlib.lean

Created Mathlib/SetTheory/Cardinal/Cofinality.lean

added theorem Cardinal.IsInaccessible.mk

added def Cardinal.IsInaccessible

added theorem Cardinal.IsLimit.aleph0_le

added theorem Cardinal.IsLimit.ne_zero

added theorem Cardinal.IsLimit.succ_lt

added def Cardinal.IsLimit

added theorem Cardinal.IsRegular.aleph0_le

added theorem Cardinal.IsRegular.cof_eq

added theorem Cardinal.IsRegular.ord_pos

added theorem Cardinal.IsRegular.pos

added def Cardinal.IsRegular

added theorem Cardinal.IsStrongLimit.isLimit

added theorem Cardinal.IsStrongLimit.ne_zero

added theorem Cardinal.IsStrongLimit.two_power_lt

added def Cardinal.IsStrongLimit

added theorem Cardinal.blsub_lt_ord_lift_of_isRegular

added theorem Cardinal.blsub_lt_ord_of_isRegular

added theorem Cardinal.bsup_lt_ord_lift_of_isRegular

added theorem Cardinal.bsup_lt_ord_of_isRegular

added theorem Cardinal.derivBFamily_lt_ord

added theorem Cardinal.derivBFamily_lt_ord_lift

added theorem Cardinal.derivFamily_lt_ord

added theorem Cardinal.derivFamily_lt_ord_lift

added theorem Cardinal.deriv_lt_ord

added theorem Cardinal.exists_infinite_fiber

added theorem Cardinal.infinite_pigeonhole_card_lt

added theorem Cardinal.isLimit_aleph0

added theorem Cardinal.isRegular_aleph'_succ

added theorem Cardinal.isRegular_aleph0

added theorem Cardinal.isRegular_aleph_one

added theorem Cardinal.isRegular_aleph_succ

added theorem Cardinal.isRegular_cof

added theorem Cardinal.isRegular_succ

added theorem Cardinal.isStrongLimit_aleph0

added theorem Cardinal.isStrongLimit_beth

added theorem Cardinal.le_range_of_union_finset_eq_top

added theorem Cardinal.lsub_lt_ord_lift_of_isRegular

added theorem Cardinal.lsub_lt_ord_of_isRegular

added theorem Cardinal.lt_cof_power

added theorem Cardinal.lt_power_cof

added theorem Cardinal.mk_bounded_subset

added theorem Cardinal.mk_subset_mk_lt_cof

added theorem Cardinal.nfpBFamily_lt_ord_lift_of_isRegular

added theorem Cardinal.nfpBFamily_lt_ord_of_isRegular

added theorem Cardinal.nfpFamily_lt_ord_lift_of_isRegular

added theorem Cardinal.nfpFamily_lt_ord_of_isRegular

added theorem Cardinal.nfp_lt_ord_of_isRegular

added theorem Cardinal.sum_lt_lift_of_isRegular

added theorem Cardinal.sum_lt_of_isRegular

added theorem Cardinal.sup_lt_ord_lift_of_isRegular

added theorem Cardinal.sup_lt_ord_of_isRegular

added theorem Cardinal.supᵢ_lt_lift_of_isRegular

added theorem Cardinal.supᵢ_lt_of_isRegular

added theorem Cardinal.univ_inaccessible

added def Order.cof

added theorem Order.cof_le

added theorem Order.cof_nonempty

added theorem Order.le_cof

added theorem Ordinal.IsFundamentalSequence.blsub_eq

added theorem Ordinal.IsFundamentalSequence.id_of_le_cof

added theorem Ordinal.IsFundamentalSequence.ord_cof

added theorem Ordinal.IsFundamentalSequence.trans

added def Ordinal.IsFundamentalSequence

added theorem Ordinal.IsNormal.cof_eq

added theorem Ordinal.IsNormal.cof_le

added theorem Ordinal.aleph'_cof

added theorem Ordinal.aleph0_le_cof

added theorem Ordinal.aleph_cof

added theorem Ordinal.blsub_lt_ord

added theorem Ordinal.blsub_lt_ord_lift

added theorem Ordinal.bsup_lt_ord

added theorem Ordinal.bsup_lt_ord_lift

added def Ordinal.cof

added theorem Ordinal.cof_add

added theorem Ordinal.cof_blsub_le

added theorem Ordinal.cof_blsub_le_lift

added theorem Ordinal.cof_bsup_le

added theorem Ordinal.cof_bsup_le_lift

added theorem Ordinal.cof_cof

added theorem Ordinal.cof_eq'

added theorem Ordinal.cof_eq

added theorem Ordinal.cof_eq_infₛ_lsub

added theorem Ordinal.cof_eq_one_iff_is_succ

added theorem Ordinal.cof_eq_zero

added theorem Ordinal.cof_le_card

added theorem Ordinal.cof_lsub_def_nonempty

added theorem Ordinal.cof_lsub_le

added theorem Ordinal.cof_lsub_le_lift

added theorem Ordinal.cof_ne_zero

added theorem Ordinal.cof_omega

added theorem Ordinal.cof_ord_le

added theorem Ordinal.cof_succ

added theorem Ordinal.cof_sup_le

added theorem Ordinal.cof_sup_le_lift

added theorem Ordinal.cof_type

added theorem Ordinal.cof_type_le

added theorem Ordinal.cof_univ

added theorem Ordinal.cof_zero

added theorem Ordinal.exists_blsub_cof

added theorem Ordinal.exists_fundamental_sequence

added theorem Ordinal.exists_lsub_cof

added theorem Ordinal.infinite_pigeonhole

added theorem Ordinal.infinite_pigeonhole_card

added theorem Ordinal.infinite_pigeonhole_set

added theorem Ordinal.le_cof_iff_blsub

added theorem Ordinal.le_cof_iff_lsub

added theorem Ordinal.le_cof_type

added theorem Ordinal.lift_cof

added theorem Ordinal.lsub_lt_ord

added theorem Ordinal.lsub_lt_ord_lift

added theorem Ordinal.lt_cof_type

added theorem Ordinal.nfpBFamily_lt_ord

added theorem Ordinal.nfpBFamily_lt_ord_lift

added theorem Ordinal.nfpFamily_lt_ord

added theorem Ordinal.nfpFamily_lt_ord_lift

added theorem Ordinal.nfp_lt_ord

added theorem Ordinal.ord_cof_eq

added theorem Ordinal.ord_cof_le

added theorem Ordinal.sup_lt_ord

added theorem Ordinal.sup_lt_ord_lift

added theorem Ordinal.supᵢ_lt

added theorem Ordinal.supᵢ_lt_lift

added theorem Ordinal.unbounded_of_unbounded_unionᵢ

added theorem Ordinal.unbounded_of_unbounded_unionₛ

added theorem RelIso.cof_eq

added theorem RelIso.cof_eq_lift

added theorem RelIso.cof_le

added theorem RelIso.cof_le_lift

added def StrictOrder.cof

added theorem StrictOrder.cof_nonempty