Aleph

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

Statistics

Metric	Count
Definitions `aleph`, `beth`, `preAleph`, `preBeth`, `termℵ_`, `termℵ₁`, `termℶ_`, `IsInitial`, `isInitialIso`, `omega`, `preOmega`, `termω_`, `termω₁`	13
Theorems `aleph0_le_aleph`, `aleph0_le_beth`, `aleph0_le_preAleph`, `aleph0_lt_aleph_one`, `aleph1_eq_lift`, `aleph1_le_lift`, `aleph1_lt_lift`, `aleph_eq_preAleph`, `aleph_le_aleph`, `aleph_le_beth`, `aleph_limit`, `aleph_lt_aleph`, `aleph_max`, `aleph_one_eq_lift`, `aleph_one_le_lift`, `aleph_one_lt_lift`, `aleph_pos`, `aleph_succ`, `aleph_toENat`, `aleph_toNat`, `aleph_zero`, `beth_eq_preBeth`, `beth_le_beth`, `beth_limit`, `beth_lt_beth`, `beth_mono`, `beth_ne_zero`, `beth_pos`, `beth_strictMono`, `beth_succ`, `beth_zero`, `countable_iff_lt_aleph_one`, `isNormal_aleph`, `isNormal_beth`, `isNormal_preAleph`, `isNormal_preBeth`, `isStrongLimit_beth`, `isStrongLimit_preBeth`, `isSuccLimit_omega`, `le_aleph_ord`, `le_beth_ord`, `le_preAleph_ord`, `le_preBeth_ord`, `lift_aleph`, `lift_beth`, `lift_eq_aleph1`, `lift_eq_aleph_one`, `lift_le_aleph1`, `lift_le_aleph_one`, `lift_lt_aleph1`, `lift_lt_aleph_one`, `lift_preAleph`, `lift_preBeth`, `lt_omega_iff_card_lt`, `mem_range_aleph_iff`, `mk_cardinal`, `ord_aleph`, `ord_preAleph`, `preAleph_le_aleph`, `preAleph_le_of_isSuccPrelimit`, `preAleph_le_of_strictMono`, `preAleph_le_preAleph`, `preAleph_le_preBeth`, `preAleph_limit`, `preAleph_lt_preAleph`, `preAleph_max`, `preAleph_nat`, `preAleph_omega0`, `preAleph_pos`, `preAleph_succ`, `preAleph_zero`, `preBeth_eq_zero`, `preBeth_inj`, `preBeth_le_beth`, `preBeth_le_preBeth`, `preBeth_limit`, `preBeth_lt_preBeth`, `preBeth_mono`, `preBeth_nat`, `preBeth_omega`, `preBeth_one`, `preBeth_pos`, `preBeth_strictMono`, `preBeth_succ`, `preBeth_zero`, `range_aleph`, `succ_aleph0`, `type_cardinal`, `card_le_card`, `card_lt_card`, `mem_range_preOmega`, `ord_card`, `card_le_aleph`, `card_le_beth`, `card_le_preAleph`, `card_le_preBeth`, `card_omega`, `card_preOmega`, `coe_preOmega`, `isInitialIso_apply`, `isInitialIso_symm_apply_coe`, `isInitial_natCast`, `isInitial_omega`, `isInitial_omega0`, `isInitial_one`, `isInitial_ord`, `isInitial_preOmega`, `isInitial_succ`, `isInitial_zero`, `isNormal_omega`, `isNormal_preOmega`, `le_omega_self`, `le_preOmega_self`, `lift_omega`, `lift_preOmega`, `mem_range_omega_iff`, `mem_range_preOmega_iff`, `not_bddAbove_isInitial`, `omega0_le_omega`, `omega0_le_preOmega_iff`, `omega0_lt_omega1`, `omega0_lt_omega_one`, `omega0_lt_preOmega_iff`, `omega_eq_preOmega`, `omega_le_omega`, `omega_lt_omega`, `omega_max`, `omega_pos`, `omega_strictMono`, `omega_zero`, `preOmega_le_of_forall_lt`, `preOmega_le_omega`, `preOmega_le_preOmega`, `preOmega_lt_preOmega`, `preOmega_max`, `preOmega_natCast`, `preOmega_ofNat`, `preOmega_omega0`, `preOmega_strictMono`, `preOmega_zero`, `range_omega`, `range_preOmega`	142
Total	155

Cardinal

Definitions

Name	Category	Theorems
`aleph` 📖	CompOp	46 math math: `aleph_le_beth`, `aleph_succ`, `aleph_pos`, `lift_eq_aleph_one`, `Ordinal.card_le_aleph`, `preAleph_le_aleph`, `aleph_one_le_continuum`, `aleph_mul_aleph0`, `aleph_add_aleph`, `lt_omega_iff_card_lt`, `aleph1_le_lift`, `le_aleph_ord`, `cardinalInterFilter_aleph_one_iff`, `aleph_le_aleph`, `ord_aleph`, `isRegular_aleph_succ`, `aleph1_lt_lift`, `isNormal_aleph`, `lift_eq_aleph1`, `aleph_max`, `range_aleph`, `aleph_one_le_lift`, `lift_le_aleph1`, `Ordinal.card_omega`, `lift_aleph`, `aleph0_le_aleph`, `aleph0_lt_aleph_one`, `aleph_mul_aleph`, `isRegular_aleph_one`, `lift_le_aleph_one`, `aleph1_eq_lift`, `aleph_eq_preAleph`, `CountableInterFilter.toCardinalInterFilter`, `aleph_one_eq_lift`, `aleph_toENat`, `countable_iff_lt_aleph_one`, `aleph_limit`, `aleph0_mul_aleph`, `lift_lt_aleph1`, `aleph_one_lt_lift`, `mem_range_aleph_iff`, `aleph_lt_aleph`, `aleph_toNat`, `succ_aleph0`, `aleph_zero`, `lift_lt_aleph_one`
`beth` 📖	CompOp	18 math math: `aleph_le_beth`, `le_beth_ord`, `aleph0_le_beth`, `beth_succ`, `beth_one`, `beth_le_beth`, `beth_zero`, `beth_mono`, `preBeth_le_beth`, `isStrongLimit_beth`, `beth_pos`, `beth_limit`, `Ordinal.card_le_beth`, `beth_strictMono`, `beth_eq_preBeth`, `lift_beth`, `beth_lt_beth`, `isNormal_beth`
`preAleph` 📖	CompOp	22 math math: `isNormal_preAleph`, `preAleph_nat`, `preAleph_le_aleph`, `Ordinal.card_le_preAleph`, `preAleph_omega0`, `le_preAleph_ord`, `preAleph_limit`, `ord_preAleph`, `preAleph_max`, `preAleph_le_of_isSuccPrelimit`, `aleph0_le_preAleph`, `preAleph_succ`, `preAleph_zero`, `preAleph_le_preAleph`, `preAleph_lt_preAleph`, `Ordinal.card_preOmega`, `preAleph_le_of_strictMono`, `preAleph_le_preBeth`, `preAleph_pos`, `aleph_eq_preAleph`, `lift_preAleph`, `isRegular_preAleph_succ`
`preBeth` 📖	CompOp	22 math math: `preBeth_omega`, `isStrongLimit_preBeth`, `preBeth_eq_zero`, `preBeth_one`, `preBeth_inj`, `lift_preBeth`, `Ordinal.card_le_preBeth`, `preBeth_zero`, `preBeth_le_beth`, `preBeth_lt_preBeth`, `preBeth_le_preBeth`, `le_preBeth_ord`, `preBeth_succ`, `preBeth_limit`, `beth_eq_preBeth`, `preAleph_le_preBeth`, `preBeth_strictMono`, `preBeth_mono`, `isNormal_preBeth`, `preBeth_pos`, `preBeth_nat`, `ZFSet.card_vonNeumann`
`termℵ_` 📖	CompOp	—
`termℵ₁` 📖	CompOp	—
`termℶ_` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aleph0_le_aleph` 📖	mathematical	—	`Cardinal` `instLE` `aleph0` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instFunLikeOrderEmbedding` `aleph`	—	`aleph_eq_preAleph` `aleph0_le_preAleph` `le_self_add` `Ordinal.canonicallyOrderedAdd`
`aleph0_le_beth` 📖	mathematical	—	`Cardinal` `instLE` `aleph0` `beth`	—	`LE.le.trans` `aleph0_le_aleph` `aleph_le_beth`
`aleph0_le_preAleph` 📖	mathematical	—	`Cardinal` `instLE` `aleph0` `DFunLike.coe` `OrderIso` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instFunLikeOrderIso` `preAleph` `Ordinal.omega0`	—	`preAleph_omega0` `preAleph_le_preAleph`
`aleph0_lt_aleph_one` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `aleph0` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `Ordinal.partialOrder` `instLE` `instFunLikeOrderEmbedding` `aleph` `Ordinal.one`	—	`succ_aleph0` `Order.lt_succ` `instNoMaxOrder`
`aleph1_eq_lift` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Ordinal` `Cardinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instLE` `instFunLikeOrderEmbedding` `aleph` `Ordinal.one` `lift`	—	`aleph_one_eq_lift`
`aleph1_le_lift` 📖	mathematical	—	`Cardinal` `instLE` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instFunLikeOrderEmbedding` `aleph` `Ordinal.one` `lift`	—	`aleph_one_le_lift`
`aleph1_lt_lift` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `Ordinal.partialOrder` `instLE` `instFunLikeOrderEmbedding` `aleph` `Ordinal.one` `lift`	—	`aleph_one_lt_lift`
`aleph_eq_preAleph` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Ordinal` `Cardinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instLE` `instFunLikeOrderEmbedding` `aleph` `OrderIso` `instFunLikeOrderIso` `preAleph` `Ordinal.add` `Ordinal.omega0`	—	—
`aleph_le_aleph` 📖	mathematical	—	`Cardinal` `instLE` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instFunLikeOrderEmbedding` `aleph`	—	`OrderEmbedding.le_iff_le`
`aleph_le_beth` 📖	mathematical	—	`Cardinal` `instLE` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instFunLikeOrderEmbedding` `aleph` `beth`	—	`preAleph_le_preBeth` `Ordinal.instAddLeftStrictMono`
`aleph_limit` 📖	mathematical	`Order.IsSuccLimit` `Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder`	`DFunLike.coe` `OrderEmbedding` `Cardinal` `Preorder.toLE` `instLE` `instFunLikeOrderEmbedding` `aleph` `iSup` `Set.Elem` `Set.Iio` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot` `Set` `Set.instMembership`	—	`Order.IsNormal.apply_of_isSuccLimit` `isNormal_aleph`
`aleph_lt_aleph` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `Ordinal.partialOrder` `instLE` `instFunLikeOrderEmbedding` `aleph`	—	`OrderEmbedding.lt_iff_lt`
`aleph_max` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Ordinal` `Cardinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instLE` `instFunLikeOrderEmbedding` `aleph` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Ordinal.instConditionallyCompleteLinearOrderBot` `instConditionallyCompleteLinearOrderBot`	—	`Monotone.map_max` `OrderEmbedding.monotone`
`aleph_one_eq_lift` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Ordinal` `Cardinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instLE` `instFunLikeOrderEmbedding` `aleph` `Ordinal.one` `lift`	—	`lift_aleph` `Ordinal.lift_one`
`aleph_one_le_lift` 📖	mathematical	—	`Cardinal` `instLE` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instFunLikeOrderEmbedding` `aleph` `Ordinal.one` `lift`	—	`lift_aleph` `Ordinal.lift_one` `lift_le`
`aleph_one_lt_lift` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `Ordinal.partialOrder` `instLE` `instFunLikeOrderEmbedding` `aleph` `Ordinal.one` `lift`	—	`lift_aleph` `Ordinal.lift_one` `lift_lt`
`aleph_pos` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instZero` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `Ordinal.partialOrder` `instLE` `instFunLikeOrderEmbedding` `aleph`	—	`LT.lt.trans_le` `aleph0_pos` `aleph0_le_aleph`
`aleph_succ` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Ordinal` `Cardinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instLE` `instFunLikeOrderEmbedding` `aleph` `Order.succ` `Ordinal.instSuccOrder` `partialOrder` `instSuccOrder`	—	`aleph_eq_preAleph` `Ordinal.add_succ` `preAleph_succ`
`aleph_toENat` 📖	mathematical	—	`DFunLike.coe` `OrderRingHom` `Cardinal` `ENat` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `PartialOrder.toPreorder` `partialOrder` `instCommSemiringENat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `OrderRingHom.instFunLike` `toENat` `OrderEmbedding` `Ordinal` `Preorder.toLE` `Ordinal.partialOrder` `instLE` `instFunLikeOrderEmbedding` `aleph` `Top.top` `instTopENat`	—	`toENat_eq_top` `aleph0_le_aleph`
`aleph_toNat` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Cardinal` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `toNat` `OrderEmbedding` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instLE` `instFunLikeOrderEmbedding` `aleph`	—	`toNat_apply_of_aleph0_le` `aleph0_le_aleph`
`aleph_zero` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Ordinal` `Cardinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instLE` `instFunLikeOrderEmbedding` `aleph` `Ordinal.zero` `aleph0`	—	`aleph_eq_preAleph` `add_zero` `preAleph_omega0`
`beth_eq_preBeth` 📖	mathematical	—	`beth` `preBeth` `Ordinal` `Ordinal.add` `Ordinal.omega0`	—	—
`beth_le_beth` 📖	mathematical	—	`Cardinal` `instLE` `beth` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder`	—	`StrictMono.le_iff_le` `beth_strictMono`
`beth_limit` 📖	mathematical	`Order.IsSuccLimit` `Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder`	`beth` `iSup` `Cardinal` `Set.Elem` `Set.Iio` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot` `Set` `Set.instMembership`	—	`Order.IsNormal.apply_of_isSuccLimit` `isNormal_beth`
`beth_lt_beth` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `beth` `Ordinal` `Ordinal.partialOrder`	—	`StrictMono.lt_iff_lt` `beth_strictMono`
`beth_mono` 📖	mathematical	—	`Monotone` `Ordinal` `Cardinal` `PartialOrder.toPreorder` `Ordinal.partialOrder` `partialOrder` `beth`	—	`StrictMono.monotone` `beth_strictMono`
`beth_ne_zero` 📖	—	—	—	—	`LT.lt.ne'` `beth_pos`
`beth_pos` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instZero` `beth`	—	`LT.lt.trans_le` `aleph0_pos` `aleph0_le_beth`
`beth_strictMono` 📖	mathematical	—	`StrictMono` `Ordinal` `Cardinal` `PartialOrder.toPreorder` `Ordinal.partialOrder` `partialOrder` `beth`	—	`StrictMono.comp` `preBeth_strictMono` `add_lt_add_right` `Ordinal.instAddLeftStrictMono`
`beth_succ` 📖	mathematical	—	`beth` `Order.succ` `Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.instSuccOrder` `Cardinal` `instPowCardinal` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `Ordinal.add_succ` `preBeth_succ`
`beth_zero` 📖	mathematical	—	`beth` `Ordinal` `Ordinal.zero` `aleph0`	—	`add_zero` `preBeth_omega`
`countable_iff_lt_aleph_one` 📖	mathematical	—	`Set.Countable` `Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `Set.Elem` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `Ordinal.partialOrder` `instLE` `instFunLikeOrderEmbedding` `aleph` `Ordinal.one`	—	`succ_aleph0` `Order.lt_succ_iff` `instNoMaxOrder` `le_aleph0_iff_set_countable`
`isNormal_aleph` 📖	mathematical	—	`Order.IsNormal` `Ordinal` `Cardinal` `Ordinal.instLinearOrder` `linearOrder` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instLE` `instFunLikeOrderEmbedding` `aleph`	—	`Order.IsNormal.comp` `Ordinal.instAddLeftStrictMono` `isNormal_preAleph` `Ordinal.isNormal_add_right`
`isNormal_beth` 📖	mathematical	—	`Order.IsNormal` `Ordinal` `Cardinal` `Ordinal.instLinearOrder` `linearOrder` `beth`	—	`Order.IsNormal.comp` `isNormal_preBeth` `Ordinal.isNormal_add_right`
`isNormal_preAleph` 📖	mathematical	—	`Order.IsNormal` `Ordinal` `Cardinal` `Ordinal.instLinearOrder` `linearOrder` `DFunLike.coe` `OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instLE` `instFunLikeOrderIso` `preAleph`	—	`OrderIso.isNormal`
`isNormal_preBeth` 📖	mathematical	—	`Order.IsNormal` `Ordinal` `Cardinal` `Ordinal.instLinearOrder` `linearOrder` `preBeth`	—	`Order.isNormal_iff` `preBeth_strictMono` `preBeth_limit` `Order.IsSuccLimit.isSuccPrelimit` `ciSup_le_iff'` `bddAbove_of_small` `small_range` `Ordinal.small_Iio`
`isStrongLimit_beth` 📖	mathematical	—	`IsStrongLimit` `beth` `Order.IsSuccPrelimit` `Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder`	—	`beth_eq_preBeth` `isStrongLimit_preBeth` `Ordinal.isSuccLimit_add_iff_of_isSuccLimit` `Ordinal.isSuccLimit_omega0`
`isStrongLimit_preBeth` 📖	mathematical	—	`IsStrongLimit` `preBeth` `Order.IsSuccLimit` `Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder`	—	`bot_eq_zero'` `Ordinal.canonicallyOrderedAdd` `Order.IsSuccLimit.ne_bot` `Nat.instAtLeastTwoHAddOfNat` `exists_lt_of_lt_ciSup'` `preBeth_limit` `Order.IsSuccLimit.isSuccPrelimit` `power_le_power_left` `two_ne_zero` `ZeroLEOneClass.neZero.two` `IsOrderedRing.toZeroLEOneClass` `isOrderedRing` `NeZero.charZero_one` `instCharZero` `addLeftMono` `LT.lt.le` `LE.le.trans_lt` `preBeth_succ` `preBeth_strictMono` `Order.IsSuccLimit.succ_lt` `Order.not_isSuccPrelimit_iff'` `Ordinal.instNoMaxOrder` `Order.not_isSuccLimit_iff` `IsMin.eq_bot` `preBeth_zero` `IsStrongLimit.two_power_lt` `Order.lt_succ`
`isSuccLimit_omega` 📖	mathematical	—	`Order.IsSuccLimit` `Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `instFunLikeOrderEmbedding` `Ordinal.omega`	—	`ord_aleph` `isSuccLimit_ord` `aleph0_le_aleph`
`le_aleph_ord` 📖	mathematical	—	`Cardinal` `instLE` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instFunLikeOrderEmbedding` `aleph` `ord`	—	`card_ord` `Ordinal.card_le_aleph`
`le_beth_ord` 📖	mathematical	—	`Cardinal` `instLE` `beth` `ord`	—	`card_ord` `Ordinal.card_le_beth`
`le_preAleph_ord` 📖	mathematical	—	`Cardinal` `instLE` `DFunLike.coe` `OrderIso` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instFunLikeOrderIso` `preAleph` `ord`	—	`card_ord` `Ordinal.card_le_preAleph`
`le_preBeth_ord` 📖	mathematical	—	`Cardinal` `instLE` `preBeth` `ord`	—	`card_ord` `Ordinal.card_le_preBeth`
`lift_aleph` 📖	mathematical	—	`lift` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Cardinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instLE` `instFunLikeOrderEmbedding` `aleph` `Ordinal.lift`	—	`lift_preAleph` `Ordinal.lift_add` `Ordinal.lift_omega0`
`lift_beth` 📖	mathematical	—	`lift` `beth` `Ordinal.lift`	—	`beth_eq_preBeth` `lift_preBeth` `Ordinal.lift_add` `Ordinal.lift_omega0`
`lift_eq_aleph1` 📖	mathematical	—	`lift` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Cardinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instLE` `instFunLikeOrderEmbedding` `aleph` `Ordinal.one`	—	`lift_eq_aleph_one`
`lift_eq_aleph_one` 📖	mathematical	—	`lift` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Cardinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instLE` `instFunLikeOrderEmbedding` `aleph` `Ordinal.one`	—	`lift_aleph` `Ordinal.lift_one`
`lift_le_aleph1` 📖	mathematical	—	`Cardinal` `instLE` `lift` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instFunLikeOrderEmbedding` `aleph` `Ordinal.one`	—	`lift_le_aleph_one`
`lift_le_aleph_one` 📖	mathematical	—	`Cardinal` `instLE` `lift` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instFunLikeOrderEmbedding` `aleph` `Ordinal.one`	—	`lift_aleph` `Ordinal.lift_one` `lift_le`
`lift_lt_aleph1` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `lift` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `Ordinal.partialOrder` `instLE` `instFunLikeOrderEmbedding` `aleph` `Ordinal.one`	—	`lift_lt_aleph_one`
`lift_lt_aleph_one` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `lift` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `Ordinal.partialOrder` `instLE` `instFunLikeOrderEmbedding` `aleph` `Ordinal.one`	—	`lift_aleph` `Ordinal.lift_one` `lift_lt`
`lift_preAleph` 📖	mathematical	—	`lift` `DFunLike.coe` `OrderIso` `Ordinal` `Cardinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instLE` `instFunLikeOrderIso` `preAleph` `Ordinal.lift`	—	`InitialSeg.eq` `isWellOrder_lt` `instWellFoundedLT`
`lift_preBeth` 📖	mathematical	—	`lift` `preBeth` `Ordinal.lift`	—	`Ordinal.wellFoundedLT` `Nat.instAtLeastTwoHAddOfNat` `preBeth_succ` `lift_power` `lift_ofNat` `Ordinal.lift_succ` `preBeth_limit` `Ordinal.isSuccPrelimit_lift` `lift_iSup` `bddAbove_of_small` `small_range` `Ordinal.small_Iio` `Set.ext` `Ordinal.mem_range_lift_of_le` `LT.lt.le` `Ordinal.lift_lt` `Set.mem_Iio`
`lt_omega_iff_card_lt` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `instFunLikeOrderEmbedding` `Ordinal.omega` `Cardinal` `partialOrder` `Ordinal.card` `instLE` `aleph`	—	`Ordinal.IsInitial.card_lt_card` `Ordinal.isInitial_omega` `Ordinal.card_omega`
`mem_range_aleph_iff` 📖	mathematical	—	`Cardinal` `Set` `Set.instMembership` `Set.range` `Ordinal` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instLE` `instFunLikeOrderEmbedding` `aleph` `aleph0`	—	`range_aleph` `Set.mem_Ici`
`mk_cardinal` 📖	mathematical	—	`Cardinal` `univ`	—	`isWellOrder_lt` `instWellFoundedLT` `type_cardinal`
`ord_aleph` 📖	mathematical	—	`ord` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Cardinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instLE` `instFunLikeOrderEmbedding` `aleph` `Ordinal.omega`	—	`ord_preAleph` `Ordinal.instAddLeftStrictMono`
`ord_preAleph` 📖	mathematical	—	`ord` `DFunLike.coe` `OrderIso` `Ordinal` `Cardinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instLE` `instFunLikeOrderIso` `preAleph` `OrderEmbedding` `instFunLikeOrderEmbedding` `Ordinal.preOmega`	—	`Ordinal.card_preOmega` `Ordinal.IsInitial.ord_card` `Ordinal.isInitial_preOmega`
`preAleph_le_aleph` 📖	mathematical	—	`Cardinal` `instLE` `DFunLike.coe` `OrderIso` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instFunLikeOrderIso` `preAleph` `OrderEmbedding` `instFunLikeOrderEmbedding` `aleph`	—	`Ordinal.instAddLeftStrictMono` `preAleph_le_preAleph` `le_add_self` `Ordinal.canonicallyOrderedAdd`
`preAleph_le_of_isSuccPrelimit` 📖	mathematical	`Order.IsSuccPrelimit` `Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder`	`Cardinal` `instLE` `DFunLike.coe` `OrderIso` `Preorder.toLE` `instFunLikeOrderIso` `preAleph`	—	`eq_or_ne` `preAleph_zero` `canonicallyOrderedAdd` `Ordinal.canonicallyOrderedAdd` `instIsEmptyFalse` `Order.IsNormal.le_iff_forall_le` `isNormal_preAleph` `bot_eq_zero'`
`preAleph_le_of_strictMono` 📖	mathematical	`StrictMono` `Ordinal` `Cardinal` `PartialOrder.toPreorder` `Ordinal.partialOrder` `partialOrder`	`instLE` `DFunLike.coe` `OrderIso` `Preorder.toLE` `instFunLikeOrderIso` `preAleph`	—	`OrderIso.symm_apply_apply` `StrictMono.id_le` `instWellFoundedLT` `StrictMono.comp` `OrderIso.strictMono`
`preAleph_le_preAleph` 📖	mathematical	—	`Cardinal` `instLE` `DFunLike.coe` `OrderIso` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instFunLikeOrderIso` `preAleph`	—	`OrderIso.le_iff_le`
`preAleph_le_preBeth` 📖	mathematical	—	`Cardinal` `instLE` `DFunLike.coe` `OrderIso` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instFunLikeOrderIso` `preAleph` `preBeth`	—	`preAleph_le_of_strictMono` `preBeth_strictMono`
`preAleph_limit` 📖	mathematical	`Order.IsSuccPrelimit` `Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder`	`DFunLike.coe` `OrderIso` `Cardinal` `Preorder.toLE` `instLE` `instFunLikeOrderIso` `preAleph` `iSup` `Set.Elem` `Set.Iio` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot` `Set` `Set.instMembership`	—	`eq_or_ne` `preAleph_zero` `ciSup_of_empty` `Ordinal.instIsEmptyIioZero` `bot_eq_zero'` `canonicallyOrderedAdd` `Order.IsNormal.apply_of_isSuccLimit` `isNormal_preAleph` `Ordinal.canonicallyOrderedAdd`
`preAleph_lt_preAleph` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `DFunLike.coe` `OrderIso` `Ordinal` `Preorder.toLE` `Ordinal.partialOrder` `instLE` `instFunLikeOrderIso` `preAleph`	—	`OrderIso.lt_iff_lt`
`preAleph_max` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Ordinal` `Cardinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instLE` `instFunLikeOrderIso` `preAleph` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Ordinal.instConditionallyCompleteLinearOrderBot` `instConditionallyCompleteLinearOrderBot`	—	`Monotone.map_max` `OrderIso.monotone`
`preAleph_nat` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Ordinal` `Cardinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instLE` `instFunLikeOrderIso` `preAleph` `AddMonoidWithOne.toNatCast` `Ordinal.addMonoidWithOne` `instNatCast`	—	`Ordinal.card_preOmega` `Ordinal.preOmega_natCast` `Ordinal.card_nat`
`preAleph_omega0` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Ordinal` `Cardinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instLE` `instFunLikeOrderIso` `preAleph` `Ordinal.omega0` `aleph0`	—	`Ordinal.card_preOmega` `Ordinal.preOmega_omega0` `Ordinal.card_omega0`
`preAleph_pos` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instZero` `DFunLike.coe` `OrderIso` `Ordinal` `Preorder.toLE` `Ordinal.partialOrder` `instLE` `instFunLikeOrderIso` `preAleph` `Ordinal.zero`	—	`preAleph_zero` `preAleph_lt_preAleph`
`preAleph_succ` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Ordinal` `Cardinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instLE` `instFunLikeOrderIso` `preAleph` `Order.succ` `Ordinal.instSuccOrder` `partialOrder` `instSuccOrder`	—	`OrderIso.map_succ`
`preAleph_zero` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Ordinal` `Cardinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instLE` `instFunLikeOrderIso` `preAleph` `Ordinal.zero` `instZero`	—	`OrderIso.map_bot`
`preBeth_eq_zero` 📖	mathematical	—	`preBeth` `Cardinal` `instZero` `Ordinal` `Ordinal.zero`	—	`preBeth_zero`
`preBeth_inj` 📖	mathematical	—	`preBeth`	—	`StrictMono.injective` `preBeth_strictMono`
`preBeth_le_beth` 📖	mathematical	—	`Cardinal` `instLE` `preBeth` `beth`	—	`preBeth_le_preBeth` `le_add_self` `Ordinal.canonicallyOrderedAdd`
`preBeth_le_preBeth` 📖	mathematical	—	`Cardinal` `instLE` `preBeth` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder`	—	`StrictMono.le_iff_le` `preBeth_strictMono`
`preBeth_limit` 📖	mathematical	`Order.IsSuccPrelimit` `Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder`	`preBeth` `iSup` `Cardinal` `Set.Elem` `Set.Iio` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot` `Set` `Set.instMembership`	—	`preBeth.eq_1` `LE.le.antisymm'` `Nat.instAtLeastTwoHAddOfNat` `ciSup_mono` `bddAbove_of_small` `small_range` `Ordinal.small_Iio` `LT.lt.le` `cantor` `ciSup_le_iff'` `preBeth_succ` `le_ciSup` `Order.IsSuccPrelimit.succ_lt`
`preBeth_lt_preBeth` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `preBeth` `Ordinal` `Ordinal.partialOrder`	—	`StrictMono.lt_iff_lt` `preBeth_strictMono`
`preBeth_mono` 📖	mathematical	—	`Monotone` `Ordinal` `Cardinal` `PartialOrder.toPreorder` `Ordinal.partialOrder` `partialOrder` `preBeth`	—	`StrictMono.monotone` `preBeth_strictMono`
`preBeth_nat` 📖	mathematical	—	`preBeth` `Ordinal` `AddMonoidWithOne.toNatCast` `Ordinal.addMonoidWithOne` `Cardinal` `instNatCast` `Nat.iterate` `Monoid.toNatPow` `Nat.instMonoid`	—	`Nat.cast_zero` `preBeth_zero` `Ordinal.natCast_succ` `Nat.instAtLeastTwoHAddOfNat` `preBeth_succ` `Function.iterate_succ_apply'` `Nat.cast_pow`
`preBeth_omega` 📖	mathematical	—	`preBeth` `Ordinal.omega0` `aleph0`	—	`le_antisymm` `preBeth_limit` `Order.IsSuccLimit.isSuccPrelimit` `Ordinal.isSuccLimit_omega0` `ciSup_le_iff'` `bddAbove_of_small` `small_range` `Ordinal.small_Iio` `Ordinal.lt_omega0` `preBeth_nat` `natCast_le_aleph0` `preAleph_omega0` `preAleph_le_preBeth`
`preBeth_one` 📖	mathematical	—	`preBeth` `Ordinal` `Ordinal.one` `Cardinal` `instOne`	—	`Nat.cast_one` `Function.iterate_one` `pow_zero` `preBeth_nat`
`preBeth_pos` 📖	mathematical	—	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instZero` `preBeth` `Ordinal` `Ordinal.partialOrder` `Ordinal.zero`	—	`preBeth_zero` `preBeth_lt_preBeth`
`preBeth_strictMono` 📖	mathematical	—	`StrictMono` `Ordinal` `Cardinal` `PartialOrder.toPreorder` `Ordinal.partialOrder` `partialOrder` `preBeth`	—	`preBeth.eq_1` `lt_ciSup_iff'` `bddAbove_of_small` `small_range` `Ordinal.small_Iio` `cantor`
`preBeth_succ` 📖	mathematical	—	`preBeth` `Order.succ` `Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.instSuccOrder` `Cardinal` `instPowCardinal` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `preBeth.eq_1` `Order.Iio_succ` `Ordinal.instNoMaxOrder` `ciSup_Iic` `power_le_power_left` `two_ne_zero` `ZeroLEOneClass.neZero.two` `IsOrderedRing.toZeroLEOneClass` `isOrderedRing` `NeZero.charZero_one` `instCharZero` `addLeftMono` `preBeth_mono`
`preBeth_zero` 📖	mathematical	—	`preBeth` `Ordinal` `Ordinal.zero` `Cardinal` `instZero`	—	`preBeth.eq_1` `ciSup_of_empty` `Ordinal.instIsEmptyIioZero` `bot_eq_zero'` `canonicallyOrderedAdd`
`range_aleph` 📖	mathematical	—	`Set.range` `Cardinal` `Ordinal` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instLE` `instFunLikeOrderEmbedding` `aleph` `Set.Ici` `partialOrder` `aleph0`	—	`Set.ext` `aleph0_le_aleph` `aleph_eq_preAleph` `Ordinal.add_sub_cancel_of_le` `aleph0_le_preAleph` `OrderIso.apply_symm_apply`
`succ_aleph0` 📖	mathematical	—	`Order.succ` `Cardinal` `PartialOrder.toPreorder` `partialOrder` `instSuccOrder` `aleph0` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `Ordinal.partialOrder` `instLE` `instFunLikeOrderEmbedding` `aleph` `Ordinal.one`	—	`aleph_zero` `aleph_succ` `Ordinal.succ_zero`
`type_cardinal` 📖	mathematical	—	`Ordinal.type` `Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `IsWellOrder` `isWellOrder_lt` `linearOrder` `instWellFoundedLT` `Ordinal.univ`	—	`isWellOrder_lt` `instWellFoundedLT` `Ordinal.wellFoundedLT` `Ordinal.univ_id`

Ordinal

Definitions

Name	Category	Theorems
`IsInitial` 📖	MathDef	16 math math: `isInitialIso_apply`, `isInitialIso_symm_apply_coe`, `isInitial_preOmega`, `range_omega`, `not_bddAbove_isInitial`, `isInitial_ord`, `mem_range_omega_iff`, `isInitial_one`, `isInitial_omega0`, `isInitial_succ`, `coe_preOmega`, `isInitial_zero`, `isInitial_omega`, `isInitial_natCast`, `mem_range_preOmega_iff`, `range_preOmega`
`isInitialIso` 📖	CompOp	2 math math: `isInitialIso_apply`, `isInitialIso_symm_apply_coe`
`omega` 📖	CompOp	29 math math: `principal_add_omega`, `omega_lt_omega`, `omega0_lt_omega_one`, `omega_zero`, `omega_le_omega`, `range_omega`, `mem_range_omega_iff`, `Cardinal.lt_omega_iff_card_lt`, `Cardinal.ord_aleph`, `preOmega_le_omega`, `principal_mul_omega`, `omega0_lt_omega1`, `omega0_le_omega`, `isInitial_omega`, `Cardinal.IsRegular.cof_omega_eq`, `card_omega`, `omega_strictMono`, `principal_opow_omega`, `MeasurableSpace.generateMeasurableRec_omega_one`, `omega_max`, `omega_pos`, `MeasurableSpace.generateMeasurableRec_omega1`, `lift_omega`, `Cardinal.isSuccLimit_omega`, `cof_omega`, `le_omega_self`, `omega_eq_preOmega`, `isNormal_omega`, `MeasurableSpace.generateMeasurable_eq_rec`
`preOmega` 📖	CompOp	23 math math: `omega0_lt_preOmega_iff`, `isInitial_preOmega`, `cof_preOmega`, `isNormal_preOmega`, `preOmega_ofNat`, `preOmega_le_omega`, `Cardinal.ord_preAleph`, `preOmega_zero`, `coe_preOmega`, `le_preOmega_self`, `omega0_le_preOmega_iff`, `lift_preOmega`, `preOmega_strictMono`, `card_preOmega`, `mem_range_preOmega_iff`, `preOmega_le_preOmega`, `preOmega_omega0`, `preOmega_lt_preOmega`, `preOmega_natCast`, `IsInitial.mem_range_preOmega`, `range_preOmega`, `preOmega_max`, `omega_eq_preOmega`
`termω_` 📖	CompOp	—
`termω₁` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_le_aleph` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `card` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instFunLikeOrderEmbedding` `Cardinal.aleph`	—	`LE.le.trans` `card_le_preAleph` `Cardinal.preAleph_le_aleph`
`card_le_beth` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `card` `Cardinal.beth`	—	`LE.le.trans` `card_le_aleph` `Cardinal.aleph_le_beth`
`card_le_preAleph` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `card` `DFunLike.coe` `OrderIso` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instFunLikeOrderIso` `Cardinal.preAleph`	—	`Eq.trans_ge` `card_preOmega` `card_le_card` `not_bddAbove_isInitial` `le_preOmega_self`
`card_le_preBeth` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `card` `Cardinal.preBeth`	—	`LE.le.trans` `card_le_preAleph` `Cardinal.preAleph_le_preBeth`
`card_omega` 📖	mathematical	—	`card` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instFunLikeOrderEmbedding` `omega` `Cardinal` `Cardinal.instLE` `Cardinal.aleph`	—	—
`card_preOmega` 📖	mathematical	—	`card` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instFunLikeOrderEmbedding` `preOmega` `OrderIso` `Cardinal` `Cardinal.instLE` `instFunLikeOrderIso` `Cardinal.preAleph`	—	—
`coe_preOmega` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instFunLikeOrderEmbedding` `preOmega` `enumOrd` `setOf` `IsInitial`	—	—
`isInitialIso_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Ordinal` `IsInitial` `Cardinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `Cardinal.instLE` `RelIso.instFunLike` `isInitialIso` `card`	—	—
`isInitialIso_symm_apply_coe` 📖	mathematical	—	`Ordinal` `IsInitial` `DFunLike.coe` `RelIso` `Cardinal` `Cardinal.instLE` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `RelIso.instFunLike` `RelIso.symm` `isInitialIso` `Cardinal.ord`	—	—
`isInitial_natCast` 📖	mathematical	—	`IsInitial` `Ordinal` `AddMonoidWithOne.toNatCast` `addMonoidWithOne`	—	`IsInitial.eq_1` `card_nat` `Cardinal.ord_nat`
`isInitial_omega` 📖	mathematical	—	`IsInitial` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instFunLikeOrderEmbedding` `omega`	—	`isInitial_preOmega` `instAddLeftStrictMono`
`isInitial_omega0` 📖	mathematical	—	`IsInitial` `omega0`	—	`IsInitial.eq_1` `card_omega0` `Cardinal.ord_aleph0`
`isInitial_one` 📖	mathematical	—	`IsInitial` `Ordinal` `one`	—	`Nat.cast_one` `isInitial_natCast`
`isInitial_ord` 📖	mathematical	—	`IsInitial` `Cardinal.ord`	—	`IsInitial.eq_1` `Cardinal.card_ord`
`isInitial_preOmega` 📖	mathematical	—	`IsInitial` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instFunLikeOrderEmbedding` `preOmega`	—	`enumOrd_mem` `not_bddAbove_isInitial`
`isInitial_succ` 📖	mathematical	—	`IsInitial` `Order.succ` `Ordinal` `PartialOrder.toPreorder` `partialOrder` `instSuccOrder` `Preorder.toLT` `omega0`	—	`Function.mtr` `ne_of_lt` `card_succ` `Cardinal.add_one_of_aleph0_le` `instNoMaxOrder` `isInitial_natCast` `lt_omega0`
`isInitial_zero` 📖	mathematical	—	`IsInitial` `Ordinal` `zero`	—	`Nat.cast_zero` `isInitial_natCast`
`isNormal_omega` 📖	mathematical	—	`Order.IsNormal` `Ordinal` `instLinearOrder` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instFunLikeOrderEmbedding` `omega`	—	`Order.IsNormal.comp` `instAddLeftStrictMono` `isNormal_preOmega` `isNormal_add_right`
`isNormal_preOmega` 📖	mathematical	—	`Order.IsNormal` `Ordinal` `instLinearOrder` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instFunLikeOrderEmbedding` `preOmega`	—	`Order.isNormal_iff` `preOmega_strictMono` `LE.le.trans` `preOmega_le_of_forall_lt` `isInitial_ord` `IsInitial.card_lt_card` `Cardinal.card_ord` `lt_of_lt_of_le` `isInitial_preOmega` `preOmega_lt_preOmega` `Order.lt_succ` `instNoMaxOrder` `card_le_card` `Order.IsSuccLimit.succ_lt` `Cardinal.ord_card_le`
`le_omega_self` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding` `omega`	—	`StrictMono.le_apply` `wellFoundedLT` `omega_strictMono`
`le_preOmega_self` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding` `preOmega`	—	`StrictMono.le_apply` `wellFoundedLT` `preOmega_strictMono`
`lift_omega` 📖	mathematical	—	`lift` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instFunLikeOrderEmbedding` `omega`	—	`lift_preOmega` `lift_add` `lift_omega0`
`lift_preOmega` 📖	mathematical	—	`lift` `DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instFunLikeOrderEmbedding` `preOmega`	—	`Cardinal.ord_preAleph` `Cardinal.lift_ord` `Cardinal.lift_preAleph`
`mem_range_omega_iff` 📖	mathematical	—	`Ordinal` `Set` `Set.instMembership` `Set.range` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instFunLikeOrderEmbedding` `omega` `omega0` `IsInitial`	—	`range_omega` `Set.mem_setOf`
`mem_range_preOmega_iff` 📖	mathematical	—	`Ordinal` `Set` `Set.instMembership` `Set.range` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instFunLikeOrderEmbedding` `preOmega` `IsInitial`	—	`range_preOmega` `Set.mem_setOf`
`not_bddAbove_isInitial` 📖	mathematical	—	`BddAbove` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `setOf` `IsInitial`	—	`isInitial_ord` `LT.lt.not_ge` `Order.lt_succ` `Cardinal.instNoMaxOrder` `Cardinal.ord_le`
`omega0_le_omega` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `omega0` `DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding` `omega`	—	`omega_zero` `omega_le_omega` `zero_le` `canonicallyOrderedAdd`
`omega0_le_preOmega_iff` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `omega0` `DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding` `preOmega`	—	`preOmega_omega0` `preOmega_le_preOmega`
`omega0_lt_omega1` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `omega0` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `instFunLikeOrderEmbedding` `omega` `one`	—	`omega0_lt_omega_one`
`omega0_lt_omega_one` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `omega0` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `instFunLikeOrderEmbedding` `omega` `one`	—	`omega_zero` `omega_lt_omega` `zero_lt_one` `instZeroLEOneClass` `instNeZeroOne`
`omega0_lt_preOmega_iff` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `omega0` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `instFunLikeOrderEmbedding` `preOmega`	—	`preOmega_omega0` `preOmega_lt_preOmega`
`omega_eq_preOmega` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instFunLikeOrderEmbedding` `omega` `preOmega` `add` `omega0`	—	—
`omega_le_omega` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding` `omega`	—	`OrderEmbedding.le_iff_le`
`omega_lt_omega` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `instFunLikeOrderEmbedding` `omega`	—	`OrderEmbedding.lt_iff_lt`
`omega_max` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instFunLikeOrderEmbedding` `omega` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot`	—	`Monotone.map_max` `OrderEmbedding.monotone`
`omega_pos` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `instFunLikeOrderEmbedding` `omega`	—	`LT.lt.trans_le` `omega0_pos` `omega0_le_omega`
`omega_strictMono` 📖	mathematical	—	`StrictMono` `Ordinal` `PartialOrder.toPreorder` `partialOrder` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `instFunLikeOrderEmbedding` `omega`	—	`OrderEmbedding.strictMono`
`omega_zero` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instFunLikeOrderEmbedding` `omega` `zero` `omega0`	—	`omega_eq_preOmega` `add_zero` `preOmega_omega0`
`preOmega_le_of_forall_lt` 📖	—	`IsInitial` `Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `instFunLikeOrderEmbedding` `preOmega`	—	—	`enumOrd_le_of_forall_lt`
`preOmega_le_omega` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding` `preOmega` `omega`	—	`instAddLeftStrictMono` `preOmega_le_preOmega` `le_add_self` `canonicallyOrderedAdd`
`preOmega_le_preOmega` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding` `preOmega`	—	`OrderEmbedding.le_iff_le`
`preOmega_lt_preOmega` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `instFunLikeOrderEmbedding` `preOmega`	—	`OrderEmbedding.lt_iff_lt`
`preOmega_max` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instFunLikeOrderEmbedding` `preOmega` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot`	—	`Monotone.map_max` `OrderEmbedding.monotone`
`preOmega_natCast` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instFunLikeOrderEmbedding` `preOmega` `AddMonoidWithOne.toNatCast` `addMonoidWithOne`	—	`preOmega_zero` `LE.le.antisymm'` `le_preOmega_self` `enumOrd_succ_le` `not_bddAbove_isInitial` `isInitial_natCast` `Eq.trans_lt` `Nat.cast_lt` `instAddLeftMono` `instZeroLEOneClass` `instCharZero` `Order.lt_succ` `Nat.instNoMaxOrder`
`preOmega_ofNat` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instFunLikeOrderEmbedding` `preOmega` `AddMonoidWithOne.toNatCast` `addMonoidWithOne`	—	`preOmega_natCast`
`preOmega_omega0` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instFunLikeOrderEmbedding` `preOmega` `omega0`	—	`apply_omega0_of_isNormal` `isNormal_preOmega` `preOmega_natCast` `iSup_natCast`
`preOmega_strictMono` 📖	mathematical	—	`StrictMono` `Ordinal` `PartialOrder.toPreorder` `partialOrder` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `instFunLikeOrderEmbedding` `preOmega`	—	`OrderEmbedding.strictMono`
`preOmega_zero` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instFunLikeOrderEmbedding` `preOmega` `zero`	—	`coe_preOmega` `enumOrd_zero` `csInf_eq_bot_of_bot_mem` `isInitial_zero`
`range_omega` 📖	mathematical	—	`Set.range` `Ordinal` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instFunLikeOrderEmbedding` `omega` `setOf` `omega0` `IsInitial`	—	`Set.ext` `omega0_le_omega` `isInitial_omega` `IsInitial.mem_range_preOmega` `omega_eq_preOmega` `add_sub_cancel_of_le` `omega0_le_preOmega_iff`
`range_preOmega` 📖	mathematical	—	`Set.range` `Ordinal` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instFunLikeOrderEmbedding` `preOmega` `setOf` `IsInitial`	—	`range_enumOrd` `not_bddAbove_isInitial`

Ordinal.IsInitial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_le_card` 📖	mathematical	`Ordinal.IsInitial`	`Cardinal` `Cardinal.instLE` `Ordinal.card` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder`	—	`LE.le.trans` `ord_card` `Cardinal.ord_le_ord` `Cardinal.ord_card_le` `Ordinal.card_le_card`
`card_lt_card` 📖	mathematical	`Ordinal.IsInitial`	`Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `Ordinal.card` `Ordinal` `Ordinal.partialOrder`	—	`lt_iff_lt_of_le_iff_le` `card_le_card`
`mem_range_preOmega` 📖	mathematical	`Ordinal.IsInitial`	`Ordinal` `Set` `Set.instMembership` `Set.range` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instFunLikeOrderEmbedding` `Ordinal.preOmega`	—	`Ordinal.mem_range_preOmega_iff`
`ord_card` 📖	mathematical	`Ordinal.IsInitial`	`Cardinal.ord` `Ordinal.card`	—	—

---

← Back to Index