FixedPoint

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

Statistics

Metric	Count
Definitions `deriv`, `derivFamily`, `nfp`, `nfpFamily`	4
Theorems `apply_le_nfp`, `apply_lt_nfp`, `deriv_fp`, `fp_iff_deriv`, `le_iff_deriv`, `nfp_fp`, `nfp_le_apply`, `add_eq_right_iff_mul_omega0_le`, `add_le_right_iff_mul_omega0_le`, `apply_le_nfp`, `apply_le_nfpFamily`, `apply_lt_nfp`, `apply_lt_nfpFamily`, `apply_lt_nfpFamily_iff`, `derivFamily_eq_enumOrd`, `derivFamily_fp`, `derivFamily_limit`, `derivFamily_strictMono`, `derivFamily_succ`, `derivFamily_zero`, `deriv_add_eq_mul_omega0_add`, `deriv_eq_derivFamily`, `deriv_eq_enumOrd`, `deriv_eq_id_of_nfp_eq_id`, `deriv_fp`, `deriv_id_of_nfp_id`, `deriv_limit`, `deriv_mul_eq_opow_omega0_mul`, `deriv_strictMono`, `deriv_succ`, `deriv_zero`, `deriv_zero_left`, `deriv_zero_right`, `eq_zero_or_opow_omega0_le_of_mul_eq_right`, `foldr_le_nfpFamily`, `fp_iff_deriv`, `fp_iff_derivFamily`, `iSup_iterate_eq_nfp`, `isNormal_deriv`, `isNormal_derivFamily`, `iterate_le_nfp`, `iterate_lt_nfp`, `le_iff_deriv`, `le_iff_derivFamily`, `le_nfp`, `le_nfpFamily`, `lt_nfpFamily_iff`, `lt_nfp_iff`, `mem_range_deriv`, `mem_range_derivFamily`, `mul_eq_right_iff_opow_omega0_dvd`, `mul_le_right_iff_opow_omega0_dvd`, `nfpFamily_eq_self`, `nfpFamily_fp`, `nfpFamily_le`, `nfpFamily_le_apply`, `nfpFamily_le_fp`, `nfpFamily_le_iff`, `nfpFamily_monotone`, `nfp_add_eq_mul_omega0`, `nfp_add_zero`, `nfp_eq_nfpFamily`, `nfp_eq_self`, `nfp_fp`, `nfp_id`, `nfp_le`, `nfp_le_apply`, `nfp_le_fp`, `nfp_le_iff`, `nfp_monotone`, `nfp_mul_eq_opow_omega0`, `nfp_mul_one`, `nfp_mul_opow_omega0_add`, `nfp_mul_zero`, `nfp_zero`, `nfp_zero_left`, `not_bddAbove_fp`, `not_bddAbove_fp_family`	78
Total	82

Ordinal

Definitions

Name	Category	Theorems
`deriv` 📖	CompOp	24 math math: `deriv_add_eq_mul_omega0_add`, `IsNormal.deriv_fp`, `deriv_strictMono`, `epsilon_eq_deriv`, `deriv_succ`, `deriv_fp`, `deriv_limit`, `isNormal_deriv`, `deriv_eq_derivFamily`, `deriv_zero`, `deriv_eq_enumOrd`, `deriv_id_of_nfp_id`, `deriv_zero_left`, `deriv_mul_eq_opow_omega0_mul`, `veblenWith_succ`, `IsNormal.fp_iff_deriv`, `mem_range_deriv`, `veblen_succ`, `deriv_zero_right`, `IsNormal.le_iff_deriv`, `deriv_eq_id_of_nfp_eq_id`, `Cardinal.deriv_lt_ord`, `fp_iff_deriv`, `le_iff_deriv`
`derivFamily` 📖	CompOp	15 math math: `fp_iff_derivFamily`, `le_iff_derivFamily`, `veblen_of_ne_zero`, `derivFamily_succ`, `derivFamily_strictMono`, `deriv_eq_derivFamily`, `isNormal_derivFamily`, `Cardinal.derivFamily_lt_ord`, `derivFamily_limit`, `Cardinal.derivFamily_lt_ord_lift`, `derivFamily_zero`, `mem_range_derivFamily`, `veblenWith_of_ne_zero`, `derivFamily_fp`, `derivFamily_eq_enumOrd`
`nfp` 📖	CompOp	39 math math: `IsNormal.apply_le_nfp`, `apply_le_nfp`, `gamma_zero_eq_nfp`, `IsNormal.nfp_le_apply`, `nfp_le_fp`, `nfp_fp`, `nfp_mul_opow_omega0_add`, `deriv_succ`, `apply_lt_nfp`, `nfp_mul_eq_opow_omega0`, `iterate_le_nfp`, `IsNormal.apply_lt_nfp`, `le_nfp`, `nfp_mul_zero`, `nfp_le_iff`, `nfp_lt_ord`, `nfp_le_apply`, `nfp_zero`, `epsilon_succ_eq_nfp`, `nfp_add_eq_mul_omega0`, `epsilon0_eq_nfp`, `epsilon_zero_eq_nfp`, `gamma0_eq_nfp`, `nfp_zero_left`, `nfp_monotone`, `nfp_id`, `lt_nfp_iff`, `nfp_eq_nfpFamily`, `nfp_le`, `nfp_mul_one`, `deriv_zero_right`, `nfp_add_zero`, `Cardinal.nfp_lt_ord_of_isRegular`, `iSup_iterate_eq_nfp`, `nfp_le_of_principal`, `iterate_lt_nfp`, `nfp_eq_self`, `gamma_succ_eq_nfp`, `IsNormal.nfp_fp`
`nfpFamily` 📖	CompOp	19 math math: `Cardinal.nfpFamily_lt_ord_of_isRegular`, `nfpFamily_eq_self`, `apply_lt_nfpFamily_iff`, `lt_nfpFamily_iff`, `foldr_le_nfpFamily`, `nfpFamily_lt_ord_lift`, `nfpFamily_le_fp`, `derivFamily_succ`, `nfpFamily_lt_ord`, `apply_le_nfpFamily`, `nfpFamily_monotone`, `Cardinal.nfpFamily_lt_ord_lift_of_isRegular`, `nfpFamily_le_iff`, `derivFamily_zero`, `nfp_eq_nfpFamily`, `nfpFamily_le_apply`, `nfpFamily_le`, `le_nfpFamily`, `nfpFamily_fp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_eq_right_iff_mul_omega0_le` 📖	mathematical	—	`Ordinal` `add` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `omega0`	—	`nfp_add_zero` `deriv_zero_right` `mem_range_deriv` `isNormal_add_right` `Order.IsNormal.monotone` `isNormal_deriv` `zero_le` `canonicallyOrderedAdd` `add_sub_cancel_of_le` `add_assoc` `mul_one_add` `leftDistribClass` `one_add_omega0`
`add_le_right_iff_mul_omega0_le` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `add` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `omega0`	—	`add_eq_right_iff_mul_omega0_le` `LE.le.ge_iff_eq'` `StrictMono.le_apply` `wellFoundedLT` `Order.IsNormal.strictMono` `isNormal_add_right`
`apply_le_nfp` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `nfp`	—	`LE.le.trans` `StrictMono.le_apply` `wellFoundedLT` `Order.IsNormal.strictMono` `nfp_fp` `Order.IsNormal.monotone`
`apply_le_nfpFamily` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `nfpFamily`	—	`LE.le.trans` `StrictMono.le_apply` `wellFoundedLT` `Order.IsNormal.strictMono` `nfpFamily_fp` `Order.IsNormal.monotone`
`apply_lt_nfp` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `nfp`	—	`apply_lt_nfpFamily_iff` `UnivLE.small` `univLE_of_max` `UnivLE.self`
`apply_lt_nfpFamily` 📖	—	`Order.IsNormal` `Ordinal` `instLinearOrder` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `nfpFamily`	—	—	`lt_nfpFamily_iff` `Order.IsNormal.strictMono`
`apply_lt_nfpFamily_iff` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `nfpFamily`	—	`lt_nfpFamily_iff` `LE.le.trans_lt` `StrictMono.le_apply` `wellFoundedLT` `Order.IsNormal.strictMono` `apply_lt_nfpFamily`
`derivFamily_eq_enumOrd` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`derivFamily` `enumOrd` `Set.iInter` `Function.fixedPoints`	—	`eq_enumOrd` `not_bddAbove_fp_family` `Order.IsNormal.strictMono` `isNormal_derivFamily` `Set.range_eq_iff` `derivFamily_fp` `fp_iff_derivFamily` `Set.mem_iInter`
`derivFamily_fp` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`derivFamily`	—	`derivFamily_zero` `nfpFamily_fp` `derivFamily_succ` `Set.Nonempty.to_subtype` `Order.IsSuccLimit.nonempty_Iio` `derivFamily_limit` `Order.IsNormal.map_iSup` `bddAbove_of_small` `small_range` `small_Iio` `eq_of_forall_ge_iff` `iSup_le_iff`
`derivFamily_limit` 📖	mathematical	`Order.IsSuccLimit` `Ordinal` `PartialOrder.toPreorder` `partialOrder`	`derivFamily` `iSup` `Set.Elem` `Set.Iio` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot` `Set` `Set.instMembership`	—	`limitRecOn_limit`
`derivFamily_strictMono` 📖	mathematical	—	`StrictMono` `Ordinal` `PartialOrder.toPreorder` `partialOrder` `derivFamily`	—	`Order.IsNormal.strictMono` `isNormal_derivFamily`
`derivFamily_succ` 📖	mathematical	—	`derivFamily` `Order.succ` `Ordinal` `PartialOrder.toPreorder` `partialOrder` `instSuccOrder` `nfpFamily`	—	`limitRecOn_succ`
`derivFamily_zero` 📖	mathematical	—	`derivFamily` `Ordinal` `zero` `nfpFamily`	—	`limitRecOn_zero`
`deriv_add_eq_mul_omega0_add` 📖	mathematical	—	`deriv` `Ordinal` `add` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `omega0`	—	`Order.IsNormal.ext` `wellFoundedLT` `isNormal_deriv` `isNormal_add_right` `bot_eq_zero` `deriv_zero_right` `add_zero` `nfp_add_zero` `deriv_succ` `add_succ` `nfp_eq_self` `add_eq_right_iff_mul_omega0_le` `LE.le.trans` `le_self_add` `canonicallyOrderedAdd` `Order.le_succ`
`deriv_eq_derivFamily` 📖	mathematical	—	`deriv` `derivFamily`	—	—
`deriv_eq_enumOrd` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`deriv` `enumOrd` `Function.fixedPoints`	—	`Set.iInter_const` `derivFamily_eq_enumOrd` `UnivLE.small` `univLE_of_max` `UnivLE.self`
`deriv_eq_id_of_nfp_eq_id` 📖	mathematical	`nfp` `Ordinal`	`deriv`	—	`Order.IsNormal.ext` `wellFoundedLT` `isNormal_deriv` `Order.IsNormal.id` `bot_eq_zero'` `canonicallyOrderedAdd` `deriv_zero_right` `deriv_succ` `instNoMaxOrder`
`deriv_fp` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`deriv`	—	`derivFamily_fp` `UnivLE.small` `univLE_of_max` `UnivLE.self`
`deriv_id_of_nfp_id` 📖	mathematical	`nfp` `Ordinal`	`deriv`	—	`deriv_eq_id_of_nfp_eq_id`
`deriv_limit` 📖	mathematical	`Order.IsSuccLimit` `Ordinal` `PartialOrder.toPreorder` `partialOrder`	`deriv` `iSup` `Preorder.toLT` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot`	—	`derivFamily_limit`
`deriv_mul_eq_opow_omega0_mul` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero`	`deriv` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `instPow` `omega0`	—	`Order.IsNormal.ext` `wellFoundedLT` `isNormal_deriv` `isNormal_mul_right` `opow_pos` `bot_eq_zero` `deriv_zero_right` `nfp_mul_zero` `MulZeroClass.mul_zero` `deriv_succ` `nfp_mul_opow_omega0_add` `zero_lt_one` `instZeroLEOneClass` `instNeZeroOne` `Order.one_le_iff_pos`
`deriv_strictMono` 📖	mathematical	—	`StrictMono` `Ordinal` `PartialOrder.toPreorder` `partialOrder` `deriv`	—	`derivFamily_strictMono` `UnivLE.small` `univLE_of_max` `UnivLE.self`
`deriv_succ` 📖	mathematical	—	`deriv` `Order.succ` `Ordinal` `PartialOrder.toPreorder` `partialOrder` `instSuccOrder` `nfp`	—	`derivFamily_succ`
`deriv_zero` 📖	mathematical	—	`deriv` `Pi.instZero` `Ordinal` `zero`	—	`deriv_eq_id_of_nfp_eq_id` `nfp_zero`
`deriv_zero_left` 📖	mathematical	—	`deriv` `Pi.instZero` `Ordinal` `zero`	—	`deriv_zero`
`deriv_zero_right` 📖	mathematical	—	`deriv` `Ordinal` `zero` `nfp`	—	`derivFamily_zero`
`eq_zero_or_opow_omega0_le_of_mul_eq_right` 📖	mathematical	`Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero`	`zero` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instPow` `omega0`	—	`eq_zero_or_pos` `canonicallyOrderedAdd` `zero_opow` `omega0_ne_zero` `zero_le` `nfp_mul_one` `nfp_le_fp` `Order.IsNormal.monotone` `isNormal_mul_right` `one_le_iff_ne_zero` `le_of_eq`
`foldr_le_nfpFamily` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `nfpFamily`	—	`le_iSup` `smallList`
`fp_iff_deriv` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`deriv`	—	`mem_range_deriv`
`fp_iff_derivFamily` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`derivFamily`	—	`le_of_eq` `LE.le.ge_iff_eq'` `StrictMono.le_apply` `wellFoundedLT` `Order.IsNormal.strictMono` `le_iff_derivFamily`
`iSup_iterate_eq_nfp` 📖	mathematical	—	`iSup` `Ordinal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instConditionallyCompleteLinearOrderBot` `Nat.iterate` `nfp`	—	`le_antisymm` `iSup_le_iff` `UnivLE.small` `univLE_of_max` `UnivLE.self` `List.foldr_const` `le_iSup` `smallList` `iSup_le`
`isNormal_deriv` 📖	mathematical	—	`Order.IsNormal` `Ordinal` `instLinearOrder` `deriv`	—	`isNormal_derivFamily` `UnivLE.small` `univLE_of_max` `UnivLE.self`
`isNormal_derivFamily` 📖	mathematical	—	`Order.IsNormal` `Ordinal` `instLinearOrder` `derivFamily`	—	`Order.IsNormal.of_succ_lt` `wellFoundedLT` `derivFamily_succ` `Order.succ_le_iff` `instNoMaxOrder` `le_nfpFamily` `derivFamily_limit` `Set.image_eq_range` `Set.Nonempty.to_subtype` `Order.IsSuccLimit.nonempty_Iio` `isLUB_ciSup` `bddAbove_of_small` `small_range` `small_Iio`
`iterate_le_nfp` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `Nat.iterate` `nfp`	—	`iSup_iterate_eq_nfp` `le_iSup` `UnivLE.small` `univLE_of_max` `UnivLE.self`
`iterate_lt_nfp` 📖	mathematical	`StrictMono` `Ordinal` `PartialOrder.toPreorder` `partialOrder` `Preorder.toLT`	`Nat.iterate` `nfp`	—	`LT.lt.trans_le` `StrictMono.iterate` `Function.iterate_succ_apply` `iterate_le_nfp`
`le_iff_deriv` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `deriv`	—	`le_iff_derivFamily` `UnivLE.small` `univLE_of_max` `UnivLE.self`
`le_iff_derivFamily` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `derivFamily`	—	`le_antisymm` `derivFamily_zero` `nfpFamily_le_fp` `Order.IsNormal.monotone` `zero_le` `canonicallyOrderedAdd` `le_or_gt` `derivFamily_succ` `Order.succ_le_of_lt` `eq_or_lt_of_le` `iSup_le_iff` `small_Iio` `not_le` `derivFamily_limit` `le_of_not_ge` `StrictMono.le_apply` `wellFoundedLT` `Order.IsNormal.strictMono` `isNormal_derivFamily` `Eq.le` `derivFamily_fp`
`le_nfp` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `nfp`	—	`iterate_le_nfp`
`le_nfpFamily` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `nfpFamily`	—	`foldr_le_nfpFamily`
`lt_nfpFamily_iff` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `nfpFamily`	—	`lt_iSup_iff` `smallList`
`lt_nfp_iff` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `nfp` `Nat.iterate`	—	`iSup_iterate_eq_nfp` `lt_iSup_iff` `UnivLE.small` `univLE_of_max` `UnivLE.self`
`mem_range_deriv` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`Set` `Set.instMembership` `Set.range` `deriv`	—	`Set.mem_range` `LE.le.ge_iff_eq'` `StrictMono.le_apply` `wellFoundedLT` `Order.IsNormal.strictMono` `le_iff_deriv`
`mem_range_derivFamily` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`Set` `Set.instMembership` `Set.range` `derivFamily`	—	`fp_iff_derivFamily`
`mul_eq_right_iff_opow_omega0_dvd` 📖	mathematical	—	`Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `instPow` `omega0`	—	`eq_zero_or_pos` `canonicallyOrderedAdd` `MulZeroClass.zero_mul` `zero_opow` `omega0_ne_zero` `zero_dvd_iff` `dvd_iff_mod_eq_zero` `eq_zero_or_opow_omega0_le_of_mul_eq_right` `add_left_cancel_iff` `instIsLeftCancelAdd` `one_add_omega0` `opow_one_add` `mul_assoc` `mul_add` `leftDistribClass` `div_add_mod` `not_lt_of_ge` `mod_lt` `opow_ne_zero` `pos_iff_ne_zero`
`mul_le_right_iff_opow_omega0_dvd` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero`	`Preorder.toLE` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `instPow` `omega0`	—	`mul_eq_right_iff_opow_omega0_dvd` `LE.le.ge_iff_eq'` `StrictMono.le_apply` `wellFoundedLT` `Order.IsNormal.strictMono` `isNormal_mul_right`
`nfpFamily_eq_self` 📖	mathematical	—	`nfpFamily`	—	`LE.le.antisymm` `iSup_le` `List.foldr_fixed'` `le_refl` `le_nfpFamily`
`nfpFamily_fp` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`nfpFamily`	—	`nfpFamily.eq_1` `Order.IsNormal.map_iSup` `bddAbove_of_small` `small_range` `smallList` `le_antisymm` `iSup_le` `le_iSup` `LE.le.trans` `StrictMono.le_apply` `wellFoundedLT` `Order.IsNormal.strictMono`
`nfpFamily_le` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder`	`nfpFamily`	—	`iSup_le`
`nfpFamily_le_apply` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `nfpFamily`	—	`Mathlib.Tactic.Contrapose.contrapose_iff₁` `apply_lt_nfpFamily_iff`
`nfpFamily_le_fp` 📖	mathematical	`Monotone` `Ordinal` `PartialOrder.toPreorder` `partialOrder` `Preorder.toLE`	`nfpFamily`	—	`iSup_le` `LE.le.trans`
`nfpFamily_le_iff` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `nfpFamily`	—	`iSup_le_iff` `smallList`
`nfpFamily_monotone` 📖	mathematical	`Monotone` `Ordinal` `PartialOrder.toPreorder` `partialOrder`	`nfpFamily`	—	`nfpFamily_le` `LE.le.trans` `List.foldr_monotone` `foldr_le_nfpFamily`
`nfp_add_eq_mul_omega0` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `omega0`	`nfp` `add`	—	`le_antisymm` `nfp_le_fp` `Order.IsNormal.monotone` `isNormal_add_right` `mul_one_add` `leftDistribClass` `one_add_omega0` `le_refl` `nfp_add_zero` `nfp_monotone` `zero_le` `canonicallyOrderedAdd`
`nfp_add_zero` 📖	mathematical	—	`nfp` `Ordinal` `add` `zero` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `omega0`	—	`Nat.cast_zero` `MulZeroClass.mul_zero` `Function.iterate_zero_apply` `Function.iterate_succ_apply'` `Nat.cast_add` `Nat.cast_one` `mul_one_add` `leftDistribClass`
`nfp_eq_nfpFamily` 📖	mathematical	—	`nfp` `nfpFamily`	—	—
`nfp_eq_self` 📖	mathematical	—	`nfp`	—	`nfpFamily_eq_self` `UnivLE.small` `univLE_of_max` `UnivLE.self`
`nfp_fp` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`nfp`	—	`nfpFamily_fp` `UnivLE.small` `univLE_of_max` `UnivLE.self`
`nfp_id` 📖	mathematical	—	`nfp` `Ordinal`	—	`Function.iterate_id` `ciSup_const`
`nfp_le` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `Nat.iterate`	`nfp`	—	`nfp_le_iff`
`nfp_le_apply` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `nfp`	—	`le_iff_le_iff_lt_iff_lt` `apply_lt_nfp`
`nfp_le_fp` 📖	mathematical	`Monotone` `Ordinal` `PartialOrder.toPreorder` `partialOrder` `Preorder.toLE`	`nfp`	—	`nfpFamily_le_fp`
`nfp_le_iff` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `nfp` `Nat.iterate`	—	`iSup_iterate_eq_nfp` `iSup_le_iff` `UnivLE.small` `univLE_of_max` `UnivLE.self`
`nfp_monotone` 📖	mathematical	`Monotone` `Ordinal` `PartialOrder.toPreorder` `partialOrder`	`nfp`	—	`nfpFamily_monotone` `UnivLE.small` `univLE_of_max` `UnivLE.self`
`nfp_mul_eq_opow_omega0` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero` `Preorder.toLE` `instPow` `omega0`	`nfp` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero`	—	`eq_zero_or_pos` `canonicallyOrderedAdd` `zero_opow` `omega0_ne_zero` `nonpos_iff_eq_zero` `MulZeroClass.zero_mul` `nfp_zero_left` `le_antisymm` `nfp_le_fp` `Order.IsNormal.monotone` `isNormal_mul_right` `opow_one_add` `one_add_omega0` `le_refl` `nfp_mul_one` `nfp_monotone` `Order.one_le_iff_pos` `instZeroLEOneClass` `instNeZeroOne`
`nfp_mul_one` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero`	`nfp` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `one` `instPow` `omega0`	—	`iSup_iterate_eq_nfp` `iSup_pow_natCast` `pow_zero` `Function.iterate_zero_apply` `Function.iterate_succ_apply'` `pow_add` `pow_one`
`nfp_mul_opow_omega0_add` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero` `Preorder.toLE` `instPow` `omega0`	`nfp` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `add` `Order.succ` `instSuccOrder`	—	`le_antisymm` `nfp_le_fp` `Order.IsNormal.monotone` `isNormal_mul_right` `mul_succ` `add_le_add_right` `instAddLeftMono` `mul_assoc` `opow_one_add` `one_add_omega0` `le_refl` `mul_eq_right_iff_opow_omega0_dvd` `nfp_fp` `mul_le_mul_right` `mulLeftMono` `le_nfp` `LT.lt.trans_le` `add_lt_add_right` `instAddLeftStrictMono` `Order.succ_le_iff` `instNoMaxOrder` `mul_lt_mul_iff_right₀` `instPosMulStrictMono` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `opow_pos` `add_zero`
`nfp_mul_zero` 📖	mathematical	—	`nfp` `Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `zero`	—	`nonpos_iff_eq_zero` `canonicallyOrderedAdd` `nfp_le_iff` `le_refl` `Function.iterate_succ_apply` `MulZeroClass.mul_zero`
`nfp_zero` 📖	mathematical	—	`nfp` `Pi.instZero` `Ordinal` `zero`	—	`nfp_zero_left`
`nfp_zero_left` 📖	mathematical	—	`nfp` `Pi.instZero` `Ordinal` `zero`	—	`iSup_iterate_eq_nfp` `LE.le.antisymm` `iSup_le` `le_refl` `Function.iterate_succ'` `canonicallyOrderedAdd` `le_iSup` `UnivLE.small` `univLE_of_max` `UnivLE.self`
`not_bddAbove_fp` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `Function.fixedPoints`	—	`Set.iInter_const` `not_bddAbove_fp_family` `UnivLE.small` `univLE_of_max` `UnivLE.self`
`not_bddAbove_fp_family` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `Set.iInter` `Function.fixedPoints`	—	`not_bddAbove_iff` `nfpFamily_fp` `LT.lt.trans_le` `Order.lt_succ` `instNoMaxOrder` `le_nfpFamily`

Ordinal.IsNormal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_le_nfp` 📖	mathematical	`Order.IsNormal` `Ordinal` `Ordinal.instLinearOrder`	`Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.nfp`	—	`Ordinal.apply_le_nfp`
`apply_lt_nfp` 📖	mathematical	`Order.IsNormal` `Ordinal` `Ordinal.instLinearOrder`	`Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.nfp`	—	`Ordinal.apply_lt_nfp`
`deriv_fp` 📖	mathematical	`Order.IsNormal` `Ordinal` `Ordinal.instLinearOrder`	`Ordinal.deriv`	—	`Ordinal.deriv_fp`
`fp_iff_deriv` 📖	mathematical	`Order.IsNormal` `Ordinal` `Ordinal.instLinearOrder`	`Ordinal.deriv`	—	`Ordinal.fp_iff_deriv`
`le_iff_deriv` 📖	mathematical	`Order.IsNormal` `Ordinal` `Ordinal.instLinearOrder`	`Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.deriv`	—	`Ordinal.le_iff_deriv`
`nfp_fp` 📖	mathematical	`Order.IsNormal` `Ordinal` `Ordinal.instLinearOrder`	`Ordinal.nfp`	—	`Ordinal.nfp_fp`
`nfp_le_apply` 📖	mathematical	`Order.IsNormal` `Ordinal` `Ordinal.instLinearOrder`	`Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.nfp`	—	`Ordinal.nfp_le_apply`

---

← Back to Index