Regular

📁 Source: Mathlib/SetTheory/Cardinal/Regular.lean

Statistics

Metric	Count
Definitions IsInaccessible, IsRegular	2
Theorems aleph0_lt, isRegular, isStrongLimit, le_cof_ord, nat_lt, ne_zero, pos, two_power_lt, univ, aleph0_le, cof_eq, cof_omega_eq, cof_ord, le_cof_ord, nat_lt, ne_zero, ord_pos, pos, blsub_lt_ord_lift_of_isRegular, blsub_lt_ord_of_isRegular, bsup_lt_ord_lift_of_isRegular, bsup_lt_ord_of_isRegular, card_biUnion_lt_iff_forall_of_isRegular, card_iUnion_lt_iff_forall_of_isRegular, card_lt_of_card_biUnion_lt, card_lt_of_card_iUnion_lt, cof_omega_add_one, cof_omega_one, cof_preOmega_add_one, derivFamily_lt_ord, derivFamily_lt_ord_lift, deriv_lt_ord, fact_isRegular_aleph0, iSup_lt_lift_of_isRegular, iSup_lt_of_isRegular, iSup_lt_ord_lift_of_isRegular, iSup_lt_ord_of_isRegular, isInaccessible_def, isRegular_aleph0, isRegular_aleph_add_one, isRegular_aleph_one, isRegular_aleph_succ, isRegular_cof, isRegular_lift_iff, isRegular_preAleph_add_one, isRegular_preAleph_succ, isRegular_succ, lsub_lt_ord_lift_of_isRegular, lsub_lt_ord_of_isRegular, nfpFamily_lt_ord_lift_of_isRegular, nfpFamily_lt_ord_of_isRegular, nfp_lt_ord_of_isRegular, sum_lt_lift_of_isRegular, sum_lt_of_isRegular, iSup_sequence_lt_omega1, iSup_sequence_lt_omega_one	56
Total	58

Cardinal

Definitions

Name	Category	Theorems
IsInaccessible 📖	CompData	2 math math: isInaccessible_def, IsInaccessible.univ
IsRegular 📖	CompData	20 math math: CategoryTheory.IsAccessibleCategory.exists_cardinal, CategoryTheory.IsLocallyPresentable.exists_cardinal, isInaccessible_def, CategoryTheory.Functor.IsAccessible.exists_cardinal, HasCardinalLT.exists_regular_cardinal, isRegular_cof, HasCardinalLT.exists_regular_cardinal_forall, CategoryTheory.MorphismProperty.smallObjectκ_isRegular, isRegular_aleph_succ, IsInaccessible.isRegular, isRegular_succ, CategoryTheory.MorphismProperty.HasSmallObjectArgument.exists_cardinal, IsRegular.lift, isRegular_aleph_one, isRegular_aleph0, isRegular_preAleph_add_one, isRegular_lift_iff, fact_isRegular_aleph0, isRegular_aleph_add_one, isRegular_preAleph_succ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
blsub_lt_ord_lift_of_isRegular 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder lift Ordinal.card Ordinal Ordinal.partialOrder ord	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Ordinal.blsub ord	—	Ordinal.blsub_lt_ord_lift IsRegular.cof_ord
blsub_lt_ord_of_isRegular 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder Ordinal.card Ordinal Ordinal.partialOrder ord	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Ordinal.blsub ord	—	Ordinal.blsub_lt_ord IsRegular.cof_ord
bsup_lt_ord_lift_of_isRegular 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder lift Ordinal.card Ordinal Ordinal.partialOrder ord	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Ordinal.bsup ord	—	Ordinal.bsup_lt_ord_lift IsRegular.cof_ord
bsup_lt_ord_of_isRegular 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder Ordinal.card Ordinal Ordinal.partialOrder ord	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Ordinal.bsup ord	—	Ordinal.bsup_lt_ord IsRegular.cof_ord
card_biUnion_lt_iff_forall_of_isRegular 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder Set.Elem	Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder Set.Elem Set.iUnion Set Set.instMembership	—	Set.biUnion_eq_iUnion card_iUnion_lt_iff_forall_of_isRegular SetCoe.forall'
card_iUnion_lt_iff_forall_of_isRegular 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder	Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder Set.Elem Set.iUnion	—	card_lt_of_card_iUnion_lt lt_of_le_of_lt mk_sUnion_le mul_lt_of_lt IsRegular.aleph0_le mk_range_le iSup_lt_of_isRegular
card_lt_of_card_biUnion_lt 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder Set.Elem Set.iUnion Set Set.instMembership	Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder Set.Elem	—	card_lt_of_card_iUnion_lt Set.biUnion_eq_iUnion
card_lt_of_card_iUnion_lt 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder Set.Elem Set.iUnion	Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder Set.Elem	—	lt_of_le_of_lt mk_le_mk_of_subset Set.subset_iUnion
cof_omega_add_one 📖	mathematical	—	Ordinal.cof DFunLike.coe OrderEmbedding Ordinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder instFunLikeOrderEmbedding Ordinal.omega Ordinal.add Ordinal.one Cardinal instLE aleph	—	IsRegular.cof_omega_eq isRegular_aleph_add_one
cof_omega_one 📖	mathematical	—	Ordinal.cof DFunLike.coe OrderEmbedding Ordinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder instFunLikeOrderEmbedding Ordinal.omega Ordinal.one Cardinal instLE aleph	—	IsRegular.cof_omega_eq isRegular_aleph_one
cof_preOmega_add_one 📖	mathematical	Ordinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder Ordinal.omega0	Ordinal.cof DFunLike.coe OrderEmbedding Ordinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder instFunLikeOrderEmbedding Ordinal.preOmega Ordinal.add Ordinal.one OrderIso Cardinal instLE instFunLikeOrderIso preAleph	—	ord_preAleph IsRegular.cof_ord isRegular_preAleph_add_one
derivFamily_lt_ord 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder Ordinal Ordinal.partialOrder ord	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Ordinal.derivFamily ord	—	derivFamily_lt_ord_lift lift_id
derivFamily_lt_ord_lift 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder lift Ordinal Ordinal.partialOrder ord	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Ordinal.derivFamily ord	—	IsRegular.cof_ord lt_of_le_of_ne IsRegular.aleph0_le Ordinal.derivFamily_zero Ordinal.nfpFamily_lt_ord_lift Ordinal.derivFamily_succ Order.IsSuccLimit.succ_lt isSuccLimit_ord LT.lt.trans Order.lt_succ Ordinal.instNoMaxOrder Ordinal.iSup_Iio_eq_bsup Ordinal.derivFamily_limit bsup_lt_ord_of_isRegular ord_lt_ord LE.le.trans_lt ord_card_le
deriv_lt_ord 📖	mathematical	IsRegular Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder ord	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Ordinal.deriv ord	—	derivFamily_lt_ord_lift mk_fintype Fintype.card_unique Nat.cast_one lift_one LT.lt.trans one_lt_aleph0 lt_of_le_of_ne IsRegular.aleph0_le
fact_isRegular_aleph0 📖	mathematical	—	Fact IsRegular aleph0	—	isRegular_aleph0
iSup_lt_lift_of_isRegular 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder lift	Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	Ordinal.iSup_lt_lift IsRegular.cof_ord
iSup_lt_of_isRegular 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder	Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	Ordinal.iSup_lt IsRegular.cof_ord
iSup_lt_ord_lift_of_isRegular 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder lift Ordinal Ordinal.partialOrder ord	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Ordinal.instConditionallyCompleteLinearOrderBot ord	—	Ordinal.iSup_lt_ord_lift IsRegular.cof_ord
iSup_lt_ord_of_isRegular 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder Ordinal Ordinal.partialOrder ord	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Ordinal.instConditionallyCompleteLinearOrderBot ord	—	Ordinal.iSup_lt_ord IsRegular.cof_ord
isInaccessible_def 📖	mathematical	—	IsInaccessible Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder aleph0 IsRegular IsStrongLimit	—	IsInaccessible.aleph0_lt IsInaccessible.isRegular IsInaccessible.isStrongLimit IsRegular.le_cof_ord IsStrongLimit.two_power_lt
isRegular_aleph0 📖	mathematical	—	IsRegular aleph0	—	le_rfl ord_aleph0 Ordinal.cof_omega0 instReflLe
isRegular_aleph_add_one 📖	mathematical	—	IsRegular DFunLike.coe OrderEmbedding Ordinal Cardinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder instLE instFunLikeOrderEmbedding aleph Ordinal.add Ordinal.one	—	succ_aleph isRegular_succ aleph0_le_aleph
isRegular_aleph_one 📖	mathematical	—	IsRegular DFunLike.coe OrderEmbedding Ordinal Cardinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder instLE instFunLikeOrderEmbedding aleph Ordinal.one	—	succ_aleph0 isRegular_succ le_rfl
isRegular_aleph_succ 📖	mathematical	—	IsRegular DFunLike.coe OrderEmbedding Ordinal Cardinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder instLE instFunLikeOrderEmbedding aleph Order.succ Ordinal.instSuccOrder	—	isRegular_aleph_add_one
isRegular_cof 📖	mathematical	Order.IsSuccLimit Ordinal PartialOrder.toPreorder Ordinal.partialOrder	IsRegular Ordinal.cof	—	Ordinal.aleph0_le_cof_iff Ordinal.one_lt_cof_iff Eq.ge Ordinal.cof_ord_cof
isRegular_lift_iff 📖	mathematical	—	IsRegular lift	—	lift_le Ordinal.lift_cof lift_ord IsRegular.lift
isRegular_preAleph_add_one 📖	mathematical	Ordinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder Ordinal.omega0	IsRegular DFunLike.coe OrderIso Ordinal Cardinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder instLE instFunLikeOrderIso preAleph Ordinal.add Ordinal.one	—	succ_preAleph isRegular_succ aleph0_le_preAleph
isRegular_preAleph_succ 📖	mathematical	Ordinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder Ordinal.omega0	IsRegular DFunLike.coe OrderIso Ordinal Cardinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder instLE instFunLikeOrderIso preAleph Order.succ Ordinal.instSuccOrder	—	isRegular_preAleph_add_one
isRegular_succ 📖	mathematical	Cardinal instLE aleph0	IsRegular Order.succ Cardinal PartialOrder.toPreorder partialOrder instSuccOrder	—	LE.le.trans Order.le_succ Order.succ_le_of_lt mk_out exists_ord_eq isSuccLimit_ord Ordinal.cof_eq' lt_imp_lt_of_le_imp_le mul_le_mul_left covariant_swap_mul_of_covariant_mul CanonicallyOrderedAdd.toMulLeftMono canonicallyOrderedAdd mul_eq_self Order.succ_le_iff instNoMaxOrder sum_const' le_trans sum_le_sum Order.lt_succ_iff lt_ord Ordinal.typein_lt_type
lsub_lt_ord_lift_of_isRegular 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder lift Ordinal Ordinal.partialOrder ord	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Ordinal.lsub ord	—	Ordinal.lsub_lt_ord_lift IsRegular.cof_ord
lsub_lt_ord_of_isRegular 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder Ordinal Ordinal.partialOrder ord	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Ordinal.lsub ord	—	Ordinal.lsub_lt_ord IsRegular.cof_ord
nfpFamily_lt_ord_lift_of_isRegular 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder lift Ordinal Ordinal.partialOrder ord	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Ordinal.nfpFamily ord	—	Ordinal.nfpFamily_lt_ord_lift IsRegular.cof_ord lt_of_le_of_ne IsRegular.aleph0_le
nfpFamily_lt_ord_of_isRegular 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder Ordinal Ordinal.partialOrder ord	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Ordinal.nfpFamily ord	—	nfpFamily_lt_ord_lift_of_isRegular lift_id
nfp_lt_ord_of_isRegular 📖	mathematical	IsRegular Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder ord	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Ordinal.nfp ord	—	Ordinal.nfp_lt_ord IsRegular.cof_ord lt_of_le_of_ne IsRegular.aleph0_le
sum_lt_lift_of_isRegular 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder lift	Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder sum	—	LE.le.trans_lt sum_le_lift_mk_mul_iSup mul_lt_of_lt IsRegular.aleph0_le iSup_lt_lift_of_isRegular
sum_lt_of_isRegular 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder	Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder sum	—	sum_lt_lift_of_isRegular lift_id

Cardinal.IsInaccessible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aleph0_lt 📖	mathematical	Cardinal.IsInaccessible	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Cardinal.aleph0	—	—
isRegular 📖	mathematical	Cardinal.IsInaccessible	Cardinal.IsRegular	—	LT.lt.le aleph0_lt le_cof_ord
isStrongLimit 📖	mathematical	Cardinal.IsInaccessible	Cardinal.IsStrongLimit	—	ne_zero two_power_lt
le_cof_ord 📖	mathematical	Cardinal.IsInaccessible	Cardinal Cardinal.instLE Ordinal.cof Cardinal.ord	—	—
nat_lt 📖	mathematical	Cardinal.IsInaccessible	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Cardinal.instNatCast	—	LT.lt.trans Cardinal.natCast_lt_aleph0 aleph0_lt
ne_zero 📖	—	Cardinal.IsInaccessible	—	—	LT.lt.ne' pos
pos 📖	mathematical	Cardinal.IsInaccessible	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Cardinal.instZero	—	LT.lt.trans Cardinal.aleph0_pos aleph0_lt
two_power_lt 📖	mathematical	Cardinal.IsInaccessible Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Cardinal.instPowCardinal instOfNatAtLeastTwo Cardinal.instNatCast Nat.instAtLeastTwoHAddOfNat	—	—
univ 📖	mathematical	—	Cardinal.IsInaccessible Cardinal.univ	—	Cardinal.aleph0_lt_univ Cardinal.ord_univ Ordinal.cof_univ instReflLe Cardinal.IsStrongLimit.two_power_lt Cardinal.IsStrongLimit.univ

Cardinal.IsRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aleph0_le 📖	mathematical	Cardinal.IsRegular	Cardinal Cardinal.instLE Cardinal.aleph0	—	—
cof_eq 📖	mathematical	Cardinal.IsRegular	Ordinal.cof Cardinal.ord	—	cof_ord
cof_omega_eq 📖	mathematical	Cardinal.IsRegular DFunLike.coe OrderEmbedding Ordinal Cardinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder Cardinal.instLE instFunLikeOrderEmbedding Cardinal.aleph	Ordinal.cof DFunLike.coe OrderEmbedding Ordinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder instFunLikeOrderEmbedding Ordinal.omega Cardinal Cardinal.instLE Cardinal.aleph	—	Cardinal.ord_aleph cof_ord
cof_ord 📖	mathematical	Cardinal.IsRegular	Ordinal.cof Cardinal.ord	—	LE.le.antisymm Ordinal.cof_ord_le le_cof_ord
le_cof_ord 📖	mathematical	Cardinal.IsRegular	Cardinal Cardinal.instLE Ordinal.cof Cardinal.ord	—	—
nat_lt 📖	mathematical	Cardinal.IsRegular	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Cardinal.instNatCast	—	lt_of_lt_of_le Cardinal.natCast_lt_aleph0 aleph0_le
ne_zero 📖	—	Cardinal.IsRegular	—	—	LT.lt.ne' pos
ord_pos 📖	mathematical	Cardinal.IsRegular	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Ordinal.zero Cardinal.ord	—	Cardinal.lt_ord Ordinal.card_zero pos
pos 📖	mathematical	Cardinal.IsRegular	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Cardinal.instZero	—	LT.lt.trans_le Cardinal.aleph0_pos aleph0_le

Ordinal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iSup_sequence_lt_omega1 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder partialOrder Cardinal.ord DFunLike.coe OrderEmbedding Cardinal Preorder.toLE Cardinal.instLE instFunLikeOrderEmbedding Cardinal.aleph one	Ordinal Preorder.toLT PartialOrder.toPreorder partialOrder iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot Cardinal.ord DFunLike.coe OrderEmbedding Cardinal Preorder.toLE Cardinal.instLE instFunLikeOrderEmbedding Cardinal.aleph one	—	iSup_sequence_lt_omega_one
iSup_sequence_lt_omega_one 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder partialOrder Cardinal.ord DFunLike.coe OrderEmbedding Cardinal Preorder.toLE Cardinal.instLE instFunLikeOrderEmbedding Cardinal.aleph one	Ordinal Preorder.toLT PartialOrder.toPreorder partialOrder iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot Cardinal.ord DFunLike.coe OrderEmbedding Cardinal Preorder.toLE Cardinal.instLE instFunLikeOrderEmbedding Cardinal.aleph one	—	iSup_lt_ord_lift Cardinal.IsRegular.cof_ord Cardinal.isRegular_aleph_one lt_of_le_of_lt Cardinal.mk_le_aleph0 instCountableULift Cardinal.aleph0_lt_aleph_one

---

← Back to Index