Principal

📁 Source: Mathlib/SetTheory/Ordinal/Principal.lean

Statistics

Metric	Count
Definitions `Principal`	1
Theorems `iSup`, `iterate_lt`, `sSup`, `add_absorp`, `add_omega0_opow`, `exists_lt_add_of_not_principal_add`, `isSuccLimit_of_principal_add`, `isSuccLimit_of_principal_mul`, `mul_eq_opow_log_succ`, `mul_lt_omega0_opow`, `mul_omega0`, `mul_omega0_dvd`, `mul_omega0_opow_opow`, `natCast_mul_omega0`, `natCast_opow_omega0`, `nfp_le_of_principal`, `not_bddAbove_principal`, `not_principal_iff`, `not_principal_iff_of_monotone`, `op_eq_self_of_principal`, `opow_omega0`, `principal_add_iff_add_left_eq_self`, `principal_add_iff_add_lt_ne_self`, `principal_add_iff_zero_or_omega0_opow`, `principal_add_mul_of_principal_add`, `principal_add_of_le_one`, `principal_add_of_principal_mul`, `principal_add_of_principal_mul_opow`, `principal_add_omega0`, `principal_add_omega0_opow`, `principal_add_one`, `principal_add_opow_of_principal_add`, `principal_iff_of_monotone`, `principal_mul_iff_le_two_or_omega0_opow_opow`, `principal_mul_iff_mul_left_eq`, `principal_mul_of_le_two`, `principal_mul_omega0`, `principal_mul_omega0_opow_opow`, `principal_mul_one`, `principal_mul_two`, `principal_one_iff`, `principal_opow_omega0`, `principal_swap_iff`, `principal_zero`	44
Total	45

Ordinal

Definitions

Name	Category	Theorems
`Principal` 📖	MathDef	31 math math: `principal_add_omega`, `principal_mul_of_le_two`, `principal_add_of_le_one`, `principal_opow_ord`, `principal_add_ord`, `principal_mul_omega0`, `IsInitial.principal_mul`, `principal_opow_omega0`, `not_bddAbove_principal`, `principal_add_iff_add_left_eq_self`, `principal_mul_ord`, `IsInitial.principal_opow`, `not_principal_iff_of_monotone`, `principal_mul_omega`, `principal_add_iff_zero_or_omega0_opow`, `principal_add_iff_add_lt_ne_self`, `not_principal_iff`, `principal_one_iff`, `principal_add_one`, `principal_mul_two`, `principal_mul_iff_mul_left_eq`, `principal_add_omega0`, `principal_mul_omega0_opow_opow`, `principal_opow_omega`, `IsInitial.principal_add`, `principal_add_omega0_opow`, `principal_swap_iff`, `principal_mul_one`, `principal_iff_of_monotone`, `principal_zero`, `principal_mul_iff_le_two_or_omega0_opow_opow`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_absorp` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instPow` `omega0` `Preorder.toLE`	`add`	—	`add_sub_cancel_of_le` `add_assoc` `add_omega0_opow`
`add_omega0_opow` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instPow` `omega0`	`add`	—	`le_antisymm` `nonpos_iff_eq_zero` `canonicallyOrderedAdd` `Order.lt_succ_iff` `instNoMaxOrder` `succ_zero` `opow_zero` `zero_add` `le_refl` `lt_mul_iff_of_isSuccLimit` `isSuccLimit_omega0` `opow_succ` `le_imp_le_of_le_of_le` `add_le_add_left` `instAddRightMono` `le_of_lt` `mul_add` `leftDistribClass` `add_omega0` `lt_opow_of_isSuccLimit` `omega0_ne_zero` `Order.IsNormal.le_iff_forall_le` `Order.IsNormal.comp` `isNormal_add_right` `isNormal_opow` `one_lt_omega0` `add_le_add_right` `instAddLeftMono` `opow_le_opow` `le_max_right` `omega0_pos` `max_lt` `LT.lt.trans_le` `opow_le_opow_right` `le_max_left` `LT.lt.le` `le_add_self`
`exists_lt_add_of_not_principal_add` 📖	mathematical	`Principal` `Ordinal` `add`	`Preorder.toLT` `PartialOrder.toPreorder` `partialOrder`	—	`not_principal_iff` `lt_of_le_of_ne` `sub_le_self` `LE.le.not_gt` `sub_le` `add_sub_cancel_of_le` `LT.lt.le`
`isSuccLimit_of_principal_add` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one` `Principal` `add`	`Order.IsSuccLimit`	—	`isSuccLimit_iff` `Order.isSuccPrelimit_iff_succ_lt` `LT.lt.ne_bot`
`isSuccLimit_of_principal_mul` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat` `Principal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero`	`Order.IsSuccLimit`	—	`Nat.instAtLeastTwoHAddOfNat` `isSuccLimit_of_principal_add` `LT.lt.trans` `Order.lt_succ` `instNoMaxOrder` `succ_one` `principal_add_of_principal_mul` `ne_of_gt`
`mul_eq_opow_log_succ` 📖	mathematical	`Principal` `Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	`instPow` `Order.succ` `instSuccOrder` `log`	—	`Nat.instAtLeastTwoHAddOfNat` `le_antisymm` `isSuccLimit_of_principal_mul` `Order.IsNormal.apply_of_isSuccLimit` `isNormal_mul_right` `pos_iff_ne_zero` `canonicallyOrderedAdd` `iSup_le_iff` `small_Iio` `LT.lt.trans` `one_lt_two` `instZeroLEOneClass` `instNeZeroOne` `instAddLeftStrictMono` `opow_pos` `zero_lt_one` `LE.le.trans` `mul_le_mul_left` `mulRightMono` `le_of_lt` `lt_mul_succ_div` `mul_assoc` `opow_succ` `mul_le_mul_right` `mulLeftMono` `LT.lt.le` `Order.IsSuccLimit.succ_lt` `div_lt` `lt_opow_succ_log_self` `le_imp_le_of_le_of_le` `opow_log_le_self` `le_refl`
`mul_lt_omega0_opow` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero` `instPow` `omega0`	`MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero`	—	`zero_or_succ_or_isSuccLimit` `lt_irrefl` `Order.IsNormal.lt_iff_exists_lt` `isNormal_mul_right` `opow_pos` `omega0_pos` `isSuccLimit_omega0` `opow_succ` `lt_imp_lt_of_le_of_le` `mul_le_mul_left` `mulRightMono` `le_of_lt` `le_refl` `mul_assoc` `mul_lt_mul_of_pos_left` `instPosMulStrictMono` `principal_mul_omega0` `isNormal_opow` `one_lt_omega0` `LE.le.trans_lt` `mul_le_mul'` `mulLeftMono` `opow_lt_opow_iff_right` `Order.IsSuccLimit.succ_lt`
`mul_omega0` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero` `omega0`	`MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero`	—	`principal_mul_iff_mul_left_eq` `principal_mul_omega0`
`mul_omega0_dvd` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero` `omega0` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `monoidWithZero`	`MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	`mul_assoc` `mul_omega0`
`mul_omega0_opow_opow` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero` `instPow` `omega0`	`MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero`	—	`eq_or_ne` `opow_zero` `opow_one` `mul_omega0` `le_antisymm` `lt_opow_of_isSuccLimit` `omega0_ne_zero` `isSuccLimit_opow_left` `isSuccLimit_omega0` `le_imp_le_of_le_of_le` `mul_le_mul_left` `mulRightMono` `le_of_lt` `le_refl` `opow_add` `add_omega0_opow` `one_mul` `Order.one_le_iff_pos` `instZeroLEOneClass` `instNeZeroOne`
`natCast_mul_omega0` 📖	mathematical	—	`Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `omega0`	—	`mul_omega0` `Nat.cast_zero` `instAddLeftMono` `instZeroLEOneClass` `instCharZero` `nat_lt_omega0`
`natCast_opow_omega0` 📖	mathematical	—	`Ordinal` `instPow` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `omega0`	—	`opow_omega0` `Nat.cast_one` `instAddLeftMono` `instZeroLEOneClass` `instCharZero` `nat_lt_omega0`
`nfp_le_of_principal` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `Principal`	`Preorder.toLE` `nfp`	—	`nfp_le` `LT.lt.le` `Principal.iterate_lt`
`not_bddAbove_principal` 📖	mathematical	—	`BddAbove` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `setOf` `Principal`	—	`LE.le.not_gt` `LE.le.trans` `le_nfp` `Order.lt_succ` `instNoMaxOrder`
`not_principal_iff` 📖	mathematical	—	`Principal` `Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `Preorder.toLE`	—	—
`not_principal_iff_of_monotone` 📖	mathematical	`Monotone` `Ordinal` `PartialOrder.toPreorder` `partialOrder` `Function.swap`	`Principal` `Preorder.toLT` `Preorder.toLE`	—	`principal_iff_of_monotone`
`op_eq_self_of_principal` 📖	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `Order.IsNormal` `instLinearOrder` `Principal` `Order.IsSuccLimit`	—	—	`LE.le.antisymm'` `StrictMono.le_apply` `wellFoundedLT` `Order.IsNormal.strictMono` `Order.IsNormal.apply_of_isSuccLimit` `iSup_le_iff` `small_Iio` `LT.lt.le`
`opow_omega0` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one` `omega0`	`instPow`	—	`LE.le.antisymm` `opow_le_of_isSuccLimit` `one_le_iff_ne_zero` `le_of_lt` `isSuccLimit_omega0` `LT.lt.le` `principal_opow_omega0` `right_le_opow`
`principal_add_iff_add_left_eq_self` 📖	mathematical	—	`Principal` `Ordinal` `add`	—	`lt_or_ge` `op_eq_self_of_principal` `isNormal_add_right` `isSuccLimit_of_principal_add` `le_one_iff` `not_lt_zero` `canonicallyOrderedAdd` `lt_one_iff_zero` `zero_add` `Order.IsNormal.strictMono`
`principal_add_iff_add_lt_ne_self` 📖	mathematical	—	`Principal` `Ordinal` `add`	—	`LT.lt.ne` `exists_lt_add_of_not_principal_add`
`principal_add_iff_zero_or_omega0_opow` 📖	mathematical	—	`Principal` `Ordinal` `add` `zero` `Set` `Set.instMembership` `Set.range` `instPow` `omega0`	—	`eq_or_ne` `principal_add_iff_add_left_eq_self` `lt_or_eq_of_le` `opow_log_le_self` `lt_opow_succ_log_self` `one_lt_omega0` `lt_mul_iff_of_isSuccLimit` `isSuccLimit_omega0` `opow_succ` `lt_omega0` `not_lt_of_ge` `Nat.cast_zero` `MulZeroClass.mul_zero` `zero_add` `Nat.cast_succ` `mul_add_one` `leftDistribClass` `add_assoc` `le_self_add` `canonicallyOrderedAdd` `add_omega0_opow`
`principal_add_mul_of_principal_add` 📖	mathematical	`Principal` `Ordinal` `add`	`MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero`	—	`eq_zero_or_pos` `canonicallyOrderedAdd` `MulZeroClass.zero_mul` `principal_zero` `MulZeroClass.mul_zero` `lt_mul_iff_of_isSuccLimit` `isSuccLimit_of_principal_add` `lt_of_le_of_ne` `succ_zero` `Order.succ_le_iff` `instNoMaxOrder` `mul_add` `leftDistribClass` `Left.add_lt_add` `instAddLeftStrictMono` `instAddRightMono`
`principal_add_of_le_one` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `one`	`Principal` `add`	—	`le_one_iff` `principal_zero` `principal_add_one`
`principal_add_of_principal_mul` 📖	mathematical	`Principal` `Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero`	`add`	—	`Nat.instAtLeastTwoHAddOfNat` `lt_or_gt_of_ne` `succ_one` `principal_add_of_le_one` `Order.lt_succ_iff` `instNoMaxOrder` `lt_of_le_of_lt` `one_add_one_eq_two` `mul_add` `leftDistribClass` `mul_one` `add_le_add` `instAddLeftMono` `instAddRightMono` `le_max_left` `le_max_right` `max_lt`
`principal_add_of_principal_mul_opow` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one` `Principal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `instPow`	`add`	—	`opow_lt_opow_iff_right` `opow_add`
`principal_add_omega0` 📖	mathematical	—	`Principal` `Ordinal` `add` `omega0`	—	`principal_add_iff_add_left_eq_self` `add_omega0`
`principal_add_omega0_opow` 📖	mathematical	—	`Principal` `Ordinal` `add` `instPow` `omega0`	—	`principal_add_iff_add_left_eq_self` `add_omega0_opow`
`principal_add_one` 📖	mathematical	—	`Principal` `Ordinal` `add` `one`	—	`principal_one_iff` `zero_add`
`principal_add_opow_of_principal_add` 📖	mathematical	`Principal` `Ordinal` `add`	`instPow`	—	`principal_add_iff_zero_or_omega0_opow` `eq_or_ne` `opow_zero` `principal_add_one` `zero_opow` `opow_mul` `principal_add_omega0_opow`
`principal_iff_of_monotone` 📖	mathematical	`Monotone` `Ordinal` `PartialOrder.toPreorder` `partialOrder` `Function.swap`	`Principal` `Preorder.toLT`	—	`le_or_gt` `LE.le.trans_lt` `LT.lt.le`
`principal_mul_iff_le_two_or_omega0_opow_opow` 📖	mathematical	—	`Principal` `Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat` `Set` `Set.instMembership` `Set.range` `instPow` `omega0`	—	`Nat.instAtLeastTwoHAddOfNat` `le_or_gt` `principal_add_iff_zero_or_omega0_opow` `principal_add_of_principal_mul` `LT.lt.ne'` `not_lt_zero` `canonicallyOrderedAdd` `principal_add_of_principal_mul_opow` `one_lt_omega0` `opow_zero` `instAddLeftMono` `instZeroLEOneClass` `instCharZero` `principal_mul_of_le_two` `principal_mul_omega0_opow_opow`
`principal_mul_iff_mul_left_eq` 📖	mathematical	—	`Principal` `Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero`	—	`Nat.instAtLeastTwoHAddOfNat` `le_or_gt` `le_antisymm` `Order.lt_succ_iff` `instNoMaxOrder` `succ_one` `LT.lt.trans_le` `succ_zero` `Order.succ_le_iff` `one_mul` `op_eq_self_of_principal` `isNormal_mul_right` `isSuccLimit_of_principal_mul` `eq_or_ne` `MulZeroClass.zero_mul` `pos_iff_ne_zero` `canonicallyOrderedAdd` `Order.IsNormal.strictMono`
`principal_mul_of_le_two` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	`Principal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero`	—	`Nat.instAtLeastTwoHAddOfNat` `lt_or_eq_of_le` `Order.lt_succ_iff` `instNoMaxOrder` `succ_one` `lt_one_iff_zero` `principal_zero` `principal_mul_one` `principal_mul_two`
`principal_mul_omega0` 📖	mathematical	—	`Principal` `Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `omega0`	—	`lt_omega0` `natCast_mul` `nat_lt_omega0`
`principal_mul_omega0_opow_opow` 📖	mathematical	—	`Principal` `Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `instPow` `omega0`	—	`principal_mul_iff_mul_left_eq` `mul_omega0_opow_opow`
`principal_mul_one` 📖	mathematical	—	`Principal` `Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `one`	—	`principal_one_iff` `MulZeroClass.zero_mul`
`principal_mul_two` 📖	mathematical	—	`Principal` `Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `succ_one` `Order.lt_succ_iff` `instNoMaxOrder` `mul_one` `mul_le_mul'` `mulLeftMono` `mulRightMono`
`principal_one_iff` 📖	mathematical	—	`Principal` `Ordinal` `one` `zero`	—	`lt_one_iff_zero` `zero_lt_one` `instZeroLEOneClass` `instNeZeroOne`
`principal_opow_omega0` 📖	mathematical	—	`Principal` `Ordinal` `instPow` `omega0`	—	`lt_omega0` `opow_natCast`
`principal_swap_iff` 📖	mathematical	—	`Principal` `Function.swap` `Ordinal`	—	—
`principal_zero` 📖	mathematical	—	`Principal` `Ordinal` `zero`	—	`canonicallyOrderedAdd`

Ordinal.Principal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iSup` 📖	mathematical	`Ordinal.Principal`	`iSup` `Ordinal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Ordinal.instConditionallyCompleteLinearOrderBot`	—	`sSup`
`iterate_lt` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.Principal`	`Nat.iterate`	—	`Function.iterate_zero` `Function.iterate_succ'`
`sSup` 📖	mathematical	`Ordinal.Principal`	`SupSet.sSup` `Ordinal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Ordinal.instConditionallyCompleteLinearOrderBot`	—	`csSup_empty` `bot_eq_zero'` `Ordinal.canonicallyOrderedAdd` `Set.eq_empty_or_nonempty` `lt_csSup_iff` `max_rec'` `lt_max_of_lt_left` `lt_max_of_lt_right` `csSup_of_not_bddAbove`

---

← Back to Index