Principal

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

Statistics

Metric	Count
Definitions `Principal`	1
Theorems `iSup`, `iterate_lt`, `sSup`, `iSup`, `iterate_lt`, `sSup`, `add_absorp`, `add_omega0_opow`, `exists_lt_add_of_not_isPrincipal_add`, `exists_lt_add_of_not_principal_add`, `isPrincipal_add_iff_add_left_eq_self`, `isPrincipal_add_iff_add_lt_ne_self`, `isPrincipal_add_iff_add_self_lt`, `isPrincipal_add_iff_zero_or_omega0_opow`, `isPrincipal_add_mul_of_isPrincipal_add`, `isPrincipal_add_of_isPrincipal_mul`, `isPrincipal_add_of_isPrincipal_mul_opow`, `isPrincipal_add_of_le_one`, `isPrincipal_add_omega0`, `isPrincipal_add_omega0_opow`, `isPrincipal_add_one`, `isPrincipal_add_opow_of_isPrincipal_add`, `isPrincipal_iff_of_monotone`, `isPrincipal_mul_iff_le_two_or_omega0_opow_opow`, `isPrincipal_mul_iff_mul_left_eq`, `isPrincipal_mul_of_le_two`, `isPrincipal_mul_omega0`, `isPrincipal_mul_omega0_opow_opow`, `isPrincipal_mul_one`, `isPrincipal_mul_two`, `isPrincipal_one_iff`, `isPrincipal_opow_omega0`, `isPrincipal_swap_iff`, `isPrincipal_zero`, `isSuccLimit_of_isPrincipal_add`, `isSuccLimit_of_isPrincipal_mul`, `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_isPrincipal`, `nfp_le_of_principal`, `not_bddAbove_principal`, `not_bddAbove_setOf_isPrincipal`, `not_isPrincipal_iff`, `not_isPrincipal_iff_of_monotone`, `not_principal_iff`, `not_principal_iff_of_monotone`, `op_eq_self_of_isPrincipal`, `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`	79
Total	80

Ordinal

Definitions

Name	Category	Theorems
`Principal` 📖	MathDef	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_absorp` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instPow` `omega0` `Preorder.toLE`	`Ordinal` `add`	—	`add_sub_cancel_of_le` `add_assoc` `add_omega0_opow`
`add_omega0_opow` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instPow` `omega0`	`Ordinal` `add` `instPow` `omega0`	—	`le_antisymm` `opow_zero` `instNoMaxOrder` `canonicallyOrderedAdd` `lt_mul_iff_of_isSuccLimit` `isSuccLimit_omega0` `opow_succ` `le_imp_le_of_le_of_le` `add_le_add_left` `instAddRightMono` `le_of_lt` `le_refl` `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_isPrincipal_add` 📖	mathematical	`IsPrincipal` `Ordinal` `add`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `add`	—	`not_isPrincipal_iff` `lt_of_le_of_ne` `sub_le_self` `LE.le.not_gt` `sub_le` `add_sub_cancel_of_le` `LT.lt.le`
`exists_lt_add_of_not_principal_add` 📖	mathematical	`IsPrincipal` `Ordinal` `add`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `add`	—	`exists_lt_add_of_not_isPrincipal_add`
`isPrincipal_add_iff_add_left_eq_self` 📖	mathematical	—	`IsPrincipal` `Ordinal` `add`	—	`lt_or_ge` `op_eq_self_of_isPrincipal` `isNormal_add_right` `isSuccLimit_of_isPrincipal_add` `Order.le_one_iff` `instNoMaxOrder` `canonicallyOrderedAdd` `not_lt_zero` `Order.lt_one_iff` `zero_add` `Order.IsNormal.strictMono`
`isPrincipal_add_iff_add_lt_ne_self` 📖	mathematical	—	`IsPrincipal` `Ordinal` `add`	—	`LT.lt.ne` `exists_lt_add_of_not_isPrincipal_add`
`isPrincipal_add_iff_add_self_lt` 📖	mathematical	—	`IsPrincipal` `Ordinal` `add` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder`	—	`isPrincipal_iff_of_monotone` `add_le_add_right` `instAddLeftMono` `add_le_add_left` `instAddRightMono`
`isPrincipal_add_iff_zero_or_omega0_opow` 📖	mathematical	—	`IsPrincipal` `Ordinal` `add` `zero` `Set` `Set.instMembership` `Set.range` `instPow` `omega0`	—	`eq_or_ne` `isPrincipal_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`
`isPrincipal_add_mul_of_isPrincipal_add` 📖	mathematical	`IsPrincipal` `Ordinal` `add`	`IsPrincipal` `Ordinal` `add` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero`	—	`eq_zero_or_pos` `canonicallyOrderedAdd` `MulZeroClass.zero_mul` `isPrincipal_zero` `MulZeroClass.mul_zero` `lt_mul_iff_of_isSuccLimit` `isSuccLimit_of_isPrincipal_add` `lt_of_le_of_ne` `Order.one_le_iff_pos` `instZeroLEOneClass` `instNeZeroOne` `mul_add` `leftDistribClass` `Left.add_lt_add` `instAddLeftStrictMono` `instAddRightMono`
`isPrincipal_add_of_isPrincipal_mul` 📖	mathematical	`IsPrincipal` `Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero`	`IsPrincipal` `Ordinal` `add`	—	`Nat.instAtLeastTwoHAddOfNat` `lt_or_gt_of_ne` `isPrincipal_add_of_le_one` `Order.lt_two_iff` `instNoMaxOrder`
`isPrincipal_add_of_isPrincipal_mul_opow` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one` `IsPrincipal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `instPow`	`IsPrincipal` `Ordinal` `add`	—	`opow_lt_opow_iff_right` `opow_add`
`isPrincipal_add_of_le_one` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `one`	`IsPrincipal` `Ordinal` `add`	—	`Order.le_one_iff` `instNoMaxOrder` `canonicallyOrderedAdd` `isPrincipal_zero` `isPrincipal_add_one`
`isPrincipal_add_omega0` 📖	mathematical	—	`IsPrincipal` `Ordinal` `add` `omega0`	—	`isPrincipal_add_iff_add_left_eq_self` `add_omega0`
`isPrincipal_add_omega0_opow` 📖	mathematical	—	`IsPrincipal` `Ordinal` `add` `instPow` `omega0`	—	`isPrincipal_add_iff_add_left_eq_self` `add_omega0_opow`
`isPrincipal_add_one` 📖	mathematical	—	`IsPrincipal` `Ordinal` `add` `one`	—	`add_zero`
`isPrincipal_add_opow_of_isPrincipal_add` 📖	mathematical	`IsPrincipal` `Ordinal` `add`	`IsPrincipal` `Ordinal` `add` `instPow`	—	`isPrincipal_add_iff_zero_or_omega0_opow` `eq_or_ne` `opow_zero` `isPrincipal_add_one` `zero_opow` `opow_mul` `isPrincipal_add_omega0_opow`
`isPrincipal_iff_of_monotone` 📖	mathematical	`Monotone` `Ordinal` `PartialOrder.toPreorder` `partialOrder` `Function.swap`	`IsPrincipal` `Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder`	—	`le_or_gt` `LE.le.trans_lt` `LT.lt.le`
`isPrincipal_mul_iff_le_two_or_omega0_opow_opow` 📖	mathematical	—	`IsPrincipal` `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` `isPrincipal_add_iff_zero_or_omega0_opow` `isPrincipal_add_of_isPrincipal_mul` `LT.lt.ne'` `not_lt_zero` `canonicallyOrderedAdd` `isPrincipal_add_of_isPrincipal_mul_opow` `one_lt_omega0` `opow_zero` `instAddLeftMono` `instZeroLEOneClass` `instCharZero` `isPrincipal_mul_of_le_two` `isPrincipal_mul_omega0_opow_opow`
`isPrincipal_mul_iff_mul_left_eq` 📖	mathematical	—	`IsPrincipal` `Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero`	—	`Nat.instAtLeastTwoHAddOfNat` `le_or_gt` `le_antisymm` `Order.lt_add_one_iff` `instNoMaxOrder` `one_add_one_eq_two` `LT.lt.trans_le` `Order.one_le_iff_pos` `instZeroLEOneClass` `instNeZeroOne` `one_mul` `op_eq_self_of_isPrincipal` `isNormal_mul_right` `isSuccLimit_of_isPrincipal_mul` `eq_or_ne` `MulZeroClass.zero_mul` `pos_iff_ne_zero` `canonicallyOrderedAdd` `Order.IsNormal.strictMono`
`isPrincipal_mul_of_le_two` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	`IsPrincipal` `Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero`	—	`Nat.instAtLeastTwoHAddOfNat` `Order.le_two_iff` `instNoMaxOrder` `canonicallyOrderedAdd` `isPrincipal_zero` `isPrincipal_mul_one` `isPrincipal_mul_two`
`isPrincipal_mul_omega0` 📖	mathematical	—	`IsPrincipal` `Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `omega0`	—	`lt_omega0` `natCast_mul` `natCast_lt_omega0`
`isPrincipal_mul_omega0_opow_opow` 📖	mathematical	—	`IsPrincipal` `Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `instPow` `omega0`	—	`isPrincipal_mul_iff_mul_left_eq` `mul_omega0_opow_opow`
`isPrincipal_mul_one` 📖	mathematical	—	`IsPrincipal` `Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `one`	—	`MulZeroClass.mul_zero`
`isPrincipal_mul_two` 📖	mathematical	—	`IsPrincipal` `Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `Order.lt_two_iff` `instNoMaxOrder` `mul_one` `mul_le_mul'` `mulLeftMono` `mulRightMono`
`isPrincipal_one_iff` 📖	mathematical	—	`IsPrincipal` `Ordinal` `one` `zero`	—	`instNoMaxOrder` `canonicallyOrderedAdd`
`isPrincipal_opow_omega0` 📖	mathematical	—	`IsPrincipal` `Ordinal` `instPow` `omega0`	—	`lt_omega0` `opow_natCast`
`isPrincipal_swap_iff` 📖	mathematical	—	`IsPrincipal` `Function.swap` `Ordinal`	—	—
`isPrincipal_zero` 📖	mathematical	—	`IsPrincipal` `Ordinal` `zero`	—	`canonicallyOrderedAdd`
`isSuccLimit_of_isPrincipal_add` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one` `IsPrincipal` `add`	`Order.IsSuccLimit` `Ordinal` `PartialOrder.toPreorder` `partialOrder`	—	`isSuccLimit_iff` `Order.isSuccPrelimit_iff_succ_lt` `LT.lt.ne_bot`
`isSuccLimit_of_isPrincipal_mul` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat` `IsPrincipal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero`	`Order.IsSuccLimit` `Ordinal` `PartialOrder.toPreorder` `partialOrder`	—	`Nat.instAtLeastTwoHAddOfNat` `isSuccLimit_of_isPrincipal_add` `LT.lt.trans` `one_lt_two` `instZeroLEOneClass` `instNeZeroOne` `instAddLeftStrictMono` `isPrincipal_add_of_isPrincipal_mul` `ne_of_gt`
`isSuccLimit_of_principal_add` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one` `IsPrincipal` `add`	`Order.IsSuccLimit` `Ordinal` `PartialOrder.toPreorder` `partialOrder`	—	`isSuccLimit_of_isPrincipal_add`
`isSuccLimit_of_principal_mul` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat` `IsPrincipal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero`	`Order.IsSuccLimit` `Ordinal` `PartialOrder.toPreorder` `partialOrder`	—	`isSuccLimit_of_isPrincipal_mul`
`mul_eq_opow_log_succ` 📖	mathematical	`IsPrincipal` `Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	`Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `instPow` `Order.succ` `PartialOrder.toPreorder` `partialOrder` `instSuccOrder` `log`	—	`Nat.instAtLeastTwoHAddOfNat` `le_antisymm` `isSuccLimit_of_isPrincipal_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` `lt_mul_iff_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`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `instPow` `omega0`	—	`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` `isPrincipal_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`	`Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `omega0`	—	`isPrincipal_mul_iff_mul_left_eq` `isPrincipal_mul_omega0`
`mul_omega0_dvd` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero` `omega0` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `monoidWithZero`	`Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero`	—	`mul_assoc` `mul_omega0`
`mul_omega0_opow_opow` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero` `instPow` `omega0`	`Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `instPow` `omega0`	—	`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` `natCast_lt_omega0`
`natCast_opow_omega0` 📖	mathematical	—	`Ordinal` `instPow` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `omega0`	—	`opow_omega0` `Nat.cast_one` `instAddLeftMono` `instZeroLEOneClass` `instCharZero` `natCast_lt_omega0`
`nfp_le_of_isPrincipal` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `IsPrincipal`	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `nfp`	—	`nfp_le` `LT.lt.le` `IsPrincipal.iterate_lt`
`nfp_le_of_principal` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `IsPrincipal`	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `nfp`	—	`nfp_le_of_isPrincipal`
`not_bddAbove_principal` 📖	mathematical	—	`BddAbove` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `setOf` `IsPrincipal`	—	`not_bddAbove_setOf_isPrincipal`
`not_bddAbove_setOf_isPrincipal` 📖	mathematical	—	`BddAbove` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `setOf` `IsPrincipal`	—	`LE.le.not_gt` `LE.le.trans` `le_nfp` `Order.lt_succ` `instNoMaxOrder`
`not_isPrincipal_iff` 📖	mathematical	—	`IsPrincipal` `Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `Preorder.toLE`	—	—
`not_isPrincipal_iff_of_monotone` 📖	mathematical	`Monotone` `Ordinal` `PartialOrder.toPreorder` `partialOrder` `Function.swap`	`IsPrincipal` `Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `Preorder.toLE`	—	`isPrincipal_iff_of_monotone`
`not_principal_iff` 📖	mathematical	—	`IsPrincipal` `Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `Preorder.toLE`	—	`not_isPrincipal_iff`
`not_principal_iff_of_monotone` 📖	mathematical	`Monotone` `Ordinal` `PartialOrder.toPreorder` `partialOrder` `Function.swap`	`IsPrincipal` `Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `Preorder.toLE`	—	`not_isPrincipal_iff_of_monotone`
`op_eq_self_of_isPrincipal` 📖	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `Order.IsNormal` `instLinearOrder` `IsPrincipal` `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`
`op_eq_self_of_principal` 📖	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `Order.IsNormal` `instLinearOrder` `IsPrincipal` `Order.IsSuccLimit`	—	—	`op_eq_self_of_isPrincipal`
`opow_omega0` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one` `omega0`	`Ordinal` `instPow` `omega0`	—	`LE.le.antisymm` `opow_le_of_isSuccLimit` `Order.one_le_iff_ne_zero` `instZeroLEOneClass` `instNeZeroOne` `canonicallyOrderedAdd` `le_of_lt` `isSuccLimit_omega0` `LT.lt.le` `isPrincipal_opow_omega0` `right_le_opow`
`principal_add_iff_add_left_eq_self` 📖	mathematical	—	`IsPrincipal` `Ordinal` `add`	—	`isPrincipal_add_iff_add_left_eq_self`
`principal_add_iff_add_lt_ne_self` 📖	mathematical	—	`IsPrincipal` `Ordinal` `add`	—	`isPrincipal_add_iff_add_lt_ne_self`
`principal_add_iff_zero_or_omega0_opow` 📖	mathematical	—	`IsPrincipal` `Ordinal` `add` `zero` `Set` `Set.instMembership` `Set.range` `instPow` `omega0`	—	`isPrincipal_add_iff_zero_or_omega0_opow`
`principal_add_mul_of_principal_add` 📖	mathematical	`IsPrincipal` `Ordinal` `add`	`IsPrincipal` `Ordinal` `add` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero`	—	`isPrincipal_add_mul_of_isPrincipal_add`
`principal_add_of_le_one` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `one`	`IsPrincipal` `Ordinal` `add`	—	`isPrincipal_add_of_le_one`
`principal_add_of_principal_mul` 📖	mathematical	`IsPrincipal` `Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero`	`IsPrincipal` `Ordinal` `add`	—	`isPrincipal_add_of_isPrincipal_mul`
`principal_add_of_principal_mul_opow` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one` `IsPrincipal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `instPow`	`IsPrincipal` `Ordinal` `add`	—	`isPrincipal_add_of_isPrincipal_mul_opow`
`principal_add_omega0` 📖	mathematical	—	`IsPrincipal` `Ordinal` `add` `omega0`	—	`isPrincipal_add_omega0`
`principal_add_omega0_opow` 📖	mathematical	—	`IsPrincipal` `Ordinal` `add` `instPow` `omega0`	—	`isPrincipal_add_omega0_opow`
`principal_add_one` 📖	mathematical	—	`IsPrincipal` `Ordinal` `add` `one`	—	`isPrincipal_add_one`
`principal_add_opow_of_principal_add` 📖	mathematical	`IsPrincipal` `Ordinal` `add`	`IsPrincipal` `Ordinal` `add` `instPow`	—	`isPrincipal_add_opow_of_isPrincipal_add`
`principal_iff_of_monotone` 📖	mathematical	`Monotone` `Ordinal` `PartialOrder.toPreorder` `partialOrder` `Function.swap`	`IsPrincipal` `Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder`	—	`isPrincipal_iff_of_monotone`
`principal_mul_iff_le_two_or_omega0_opow_opow` 📖	mathematical	—	`IsPrincipal` `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`	—	`isPrincipal_mul_iff_le_two_or_omega0_opow_opow`
`principal_mul_iff_mul_left_eq` 📖	mathematical	—	`IsPrincipal` `Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero`	—	`isPrincipal_mul_iff_mul_left_eq`
`principal_mul_of_le_two` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	`IsPrincipal` `Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero`	—	`isPrincipal_mul_of_le_two`
`principal_mul_omega0` 📖	mathematical	—	`IsPrincipal` `Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `omega0`	—	`isPrincipal_mul_omega0`
`principal_mul_omega0_opow_opow` 📖	mathematical	—	`IsPrincipal` `Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `instPow` `omega0`	—	`isPrincipal_mul_omega0_opow_opow`
`principal_mul_one` 📖	mathematical	—	`IsPrincipal` `Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `one`	—	`isPrincipal_mul_one`
`principal_mul_two` 📖	mathematical	—	`IsPrincipal` `Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat`	—	`isPrincipal_mul_two`
`principal_one_iff` 📖	mathematical	—	`IsPrincipal` `Ordinal` `one` `zero`	—	`isPrincipal_one_iff`
`principal_opow_omega0` 📖	mathematical	—	`IsPrincipal` `Ordinal` `instPow` `omega0`	—	`isPrincipal_opow_omega0`
`principal_swap_iff` 📖	mathematical	—	`IsPrincipal` `Function.swap` `Ordinal`	—	`isPrincipal_swap_iff`
`principal_zero` 📖	mathematical	—	`IsPrincipal` `Ordinal` `zero`	—	`isPrincipal_zero`

Ordinal.IsPrincipal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iSup` 📖	mathematical	`Ordinal.IsPrincipal`	`Ordinal.IsPrincipal` `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.IsPrincipal`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Nat.iterate`	—	`Function.iterate_zero` `Function.iterate_succ'`
`sSup` 📖	mathematical	`Ordinal.IsPrincipal`	`Ordinal.IsPrincipal` `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`

Ordinal.Principal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iSup` 📖	mathematical	`Ordinal.IsPrincipal`	`Ordinal.IsPrincipal` `iSup` `Ordinal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Ordinal.instConditionallyCompleteLinearOrderBot`	—	`Ordinal.IsPrincipal.iSup`
`iterate_lt` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.IsPrincipal`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Nat.iterate`	—	`Ordinal.IsPrincipal.iterate_lt`
`sSup` 📖	mathematical	`Ordinal.IsPrincipal`	`Ordinal.IsPrincipal` `SupSet.sSup` `Ordinal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Ordinal.instConditionallyCompleteLinearOrderBot`	—	`Ordinal.IsPrincipal.sSup`

---

← Back to Index