Regular

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

Statistics

Metric	Count
Definitions IsInaccessible, IsRegular	2
Theorems aleph0_lt, isRegular, isStrongLimit, nat_lt, ne_zero, pos, univ, aleph0_le, cof_eq, cof_omega_eq, 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, 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, isInaccesible_def, isInaccessible_def, isRegular_aleph0, isRegular_aleph_one, isRegular_aleph_succ, isRegular_cof, isRegular_lift_iff, 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	48
Total	50

Cardinal

Definitions

Name	Category	Theorems
IsInaccessible 📖	MathDef	3 math math: isInaccessible_def, IsInaccessible.univ, isInaccesible_def
IsRegular 📖	MathDef	14 math math: isInaccessible_def, HasCardinalLT.exists_regular_cardinal, isRegular_cof, HasCardinalLT.exists_regular_cardinal_forall, CategoryTheory.MorphismProperty.smallObjectκ_isRegular, isRegular_aleph_succ, IsInaccessible.isRegular, isRegular_succ, isRegular_aleph_one, isRegular_aleph0, isInaccesible_def, isRegular_lift_iff, fact_isRegular_aleph0, 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.blsub	—	Ordinal.blsub_lt_ord_lift IsRegular.cof_eq
blsub_lt_ord_of_isRegular 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder Ordinal.card Ordinal Ordinal.partialOrder ord	Ordinal.blsub	—	Ordinal.blsub_lt_ord IsRegular.cof_eq
bsup_lt_ord_lift_of_isRegular 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder lift Ordinal.card Ordinal Ordinal.partialOrder ord	Ordinal.bsup	—	Ordinal.bsup_lt_ord_lift IsRegular.cof_eq
bsup_lt_ord_of_isRegular 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder Ordinal.card Ordinal Ordinal.partialOrder ord	Ordinal.bsup	—	Ordinal.bsup_lt_ord IsRegular.cof_eq
card_biUnion_lt_iff_forall_of_isRegular 📖	mathematical	IsRegular 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	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 📖	—	Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder Set.Elem Set.iUnion Set Set.instMembership	—	—	card_lt_of_card_iUnion_lt Set.biUnion_eq_iUnion
card_lt_of_card_iUnion_lt 📖	—	Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder Set.Elem Set.iUnion	—	—	lt_of_le_of_lt mk_le_mk_of_subset Set.subset_iUnion
derivFamily_lt_ord 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder Ordinal Ordinal.partialOrder ord	Ordinal.derivFamily	—	derivFamily_lt_ord_lift lift_id
derivFamily_lt_ord_lift 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder lift Ordinal Ordinal.partialOrder ord	Ordinal.derivFamily	—	IsRegular.cof_eq lt_of_le_of_ne 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.deriv	—	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
fact_isRegular_aleph0 📖	mathematical	—	Fact IsRegular aleph0	—	isRegular_aleph0
iSup_lt_lift_of_isRegular 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder lift	iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	Ordinal.iSup_lt_lift IsRegular.cof_eq
iSup_lt_of_isRegular 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder	iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	Ordinal.iSup_lt IsRegular.cof_eq
iSup_lt_ord_lift_of_isRegular 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder lift Ordinal Ordinal.partialOrder ord	iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Ordinal.instConditionallyCompleteLinearOrderBot	—	Ordinal.iSup_lt_ord_lift IsRegular.cof_eq
iSup_lt_ord_of_isRegular 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder Ordinal Ordinal.partialOrder ord	iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Ordinal.instConditionallyCompleteLinearOrderBot	—	Ordinal.iSup_lt_ord IsRegular.cof_eq
isInaccesible_def 📖	mathematical	—	IsInaccessible Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder aleph0 IsRegular IsStrongLimit	—	isInaccessible_def
isInaccessible_def 📖	mathematical	—	IsInaccessible Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder aleph0 IsRegular IsStrongLimit	—	IsInaccessible.aleph0_lt IsInaccessible.isRegular IsInaccessible.isStrongLimit IsStrongLimit.two_power_lt
isRegular_aleph0 📖	mathematical	—	IsRegular aleph0	—	le_rfl ord_aleph0 Ordinal.cof_omega0
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	—	aleph_succ isRegular_succ aleph0_le_aleph
isRegular_cof 📖	mathematical	Order.IsSuccLimit Ordinal PartialOrder.toPreorder Ordinal.partialOrder	IsRegular Ordinal.cof	—	Ordinal.aleph0_le_cof Eq.ge Ordinal.cof_cof
isRegular_lift_iff 📖	mathematical	—	IsRegular lift	—	lift_le Ordinal.lift_cof lift_ord IsRegular.lift
isRegular_preAleph_succ 📖	mathematical	Ordinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder Ordinal.omega0	IsRegular DFunLike.coe OrderIso Cardinal instLE instFunLikeOrderIso preAleph Order.succ Ordinal.instSuccOrder	—	preAleph_succ isRegular_succ aleph0_le_preAleph
isRegular_succ 📖	mathematical	Cardinal instLE aleph0	IsRegular Order.succ PartialOrder.toPreorder partialOrder instSuccOrder	—	LE.le.trans Order.le_succ Order.succ_le_of_lt mk_out 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.lsub	—	Ordinal.lsub_lt_ord_lift IsRegular.cof_eq
lsub_lt_ord_of_isRegular 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder Ordinal Ordinal.partialOrder ord	Ordinal.lsub	—	Ordinal.lsub_lt_ord IsRegular.cof_eq
nfpFamily_lt_ord_lift_of_isRegular 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder lift Ordinal Ordinal.partialOrder ord	Ordinal.nfpFamily	—	Ordinal.nfpFamily_lt_ord_lift IsRegular.cof_eq lt_of_le_of_ne
nfpFamily_lt_ord_of_isRegular 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder Ordinal Ordinal.partialOrder ord	Ordinal.nfpFamily	—	nfpFamily_lt_ord_lift_of_isRegular lift_id
nfp_lt_ord_of_isRegular 📖	mathematical	IsRegular Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder ord	Ordinal.nfp	—	Ordinal.nfp_lt_ord IsRegular.cof_eq lt_of_le_of_ne
sum_lt_lift_of_isRegular 📖	mathematical	IsRegular Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder lift	sum	—	LE.le.trans_lt sum_le_lift_mk_mul_iSup mul_lt_of_lt iSup_lt_lift_of_isRegular
sum_lt_of_isRegular 📖	mathematical	IsRegular 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
isStrongLimit 📖	mathematical	Cardinal.IsInaccessible	Cardinal.IsStrongLimit	—	ne_zero
nat_lt 📖	mathematical	Cardinal.IsInaccessible	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Cardinal.instNatCast	—	LT.lt.trans Cardinal.natCast_lt_aleph0
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
univ 📖	mathematical	—	Cardinal.IsInaccessible Cardinal.univ	—	Cardinal.aleph0_lt_univ Cardinal.ord_univ Ordinal.cof_univ 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	—	LE.le.antisymm Ordinal.cof_ord_le
cof_omega_eq 📖	mathematical	Cardinal.IsRegular DFunLike.coe OrderEmbedding Ordinal Cardinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder Cardinal.instLE instFunLikeOrderEmbedding Cardinal.aleph	Ordinal.cof Ordinal.omega	—	Cardinal.ord_aleph cof_eq
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

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	iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	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	iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	iSup_lt_ord_lift Cardinal.IsRegular.cof_eq Cardinal.isRegular_aleph_one lt_of_le_of_lt Cardinal.mk_le_aleph0 instCountableULift Cardinal.aleph0_lt_aleph_one

---

← Back to Index