Veblen

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

Statistics

Metric	Count
Definitions `epsilon`, `gamma`, `invVeblen₁`, `invVeblen₂`, `termΓ_`, `termΓ₀`, `termε_`, `termε₀`, `veblen`, `veblenWith`	10
Theorems `veblenWith`, `veblenWith_zero`, `apply_lt_veblenWith_apply_iff`, `cmp_veblen`, `cmp_veblenWith`, `epsilon0_eq_nfp`, `epsilon0_le_of_omega0_opow_le`, `epsilon0_lt_gamma`, `epsilon_eq_deriv`, `epsilon_pos`, `epsilon_succ_eq_nfp`, `epsilon_zero_eq_nfp`, `epsilon_zero_le_of_omega0_opow_le`, `epsilon_zero_lt_gamma`, `gamma0_eq_nfp`, `gamma0_le_of_veblen_le`, `gamma_inj`, `gamma_le_gamma`, `gamma_lt_gamma`, `gamma_ne_zero`, `gamma_pos`, `gamma_succ_eq_nfp`, `gamma_zero_eq_nfp`, `gamma_zero_le_of_veblen_le`, `invVeblen₁_epsilon`, `invVeblen₁_eq_iff`, `invVeblen₁_gamma`, `invVeblen₁_le`, `invVeblen₁_lt_iff`, `invVeblen₁_of_lt_opow`, `invVeblen₁_veblen`, `invVeblen₁_zero`, `invVeblen₂_epsilon`, `invVeblen₂_eq_iff`, `invVeblen₂_gamma`, `invVeblen₂_le`, `invVeblen₂_le_iff`, `invVeblen₂_lt`, `invVeblen₂_lt_iff`, `invVeblen₂_of_lt_opow`, `invVeblen₂_veblen`, `invVeblen₂_zero`, `isNormal_gamma`, `isNormal_veblen`, `isNormal_veblenWith`, `isNormal_veblenWith'`, `isNormal_veblenWith_zero`, `isNormal_veblen_zero`, `iterate_omega0_opow_lt_epsilon0`, `iterate_omega0_opow_lt_epsilon_zero`, `iterate_veblen_lt_gamma0`, `iterate_veblen_lt_gamma_zero`, `le_invVeblen₂_iff`, `left_le_veblen`, `left_le_veblenWith`, `lt_epsilon0`, `lt_epsilon_zero`, `lt_gamma0`, `lt_gamma_zero`, `lt_invVeblen₂_iff`, `lt_veblen`, `lt_veblen_iff_invVeblen₁_le`, `lt_veblen_invVeblen₁`, `mem_range_gamma`, `mem_range_veblen`, `mem_range_veblenWith`, `mem_range_veblen_iff_le_invVeblen₁`, `monotone_gamma`, `natCast_lt_epsilon`, `natCast_lt_gamma`, `omega0_lt_epsilon`, `omega0_lt_gamma`, `omega0_opow_epsilon`, `opow_lt_veblen_opow_iff`, `right_le_veblen`, `right_le_veblenWith`, `strictMono_gamma`, `veblenWith_apply_eq_apply_iff`, `veblenWith_eq_self_of_le`, `veblenWith_eq_veblenWith_iff`, `veblenWith_inj`, `veblenWith_injective`, `veblenWith_le_veblenWith_iff`, `veblenWith_le_veblenWith_iff_right`, `veblenWith_left_monotone`, `veblenWith_lt_veblenWith_iff`, `veblenWith_lt_veblenWith_iff_right`, `veblenWith_lt_veblenWith_veblenWith_iff`, `veblenWith_mem_range`, `veblenWith_of_ne_zero`, `veblenWith_pos`, `veblenWith_right_strictMono`, `veblenWith_succ`, `veblenWith_veblenWith_eq_veblenWith_iff`, `veblenWith_veblenWith_of_lt`, `veblenWith_zero`, `veblenWith_zero_inj`, `veblenWith_zero_le_veblenWith_zero`, `veblenWith_zero_lt_veblenWith_zero`, `veblenWith_zero_strictMono`, `veblen_eq_of_lt_invVeblen₁`, `veblen_eq_opow_iff`, `veblen_eq_self_of_le`, `veblen_eq_veblen_iff`, `veblen_gamma_zero`, `veblen_inj`, `veblen_injective`, `veblen_invVeblen₁_invVeblen₂`, `veblen_le_veblen_iff`, `veblen_le_veblen_iff_right`, `veblen_left_monotone`, `veblen_lt_veblen_iff`, `veblen_lt_veblen_iff_right`, `veblen_lt_veblen_veblen_iff`, `veblen_mem_range_opow`, `veblen_of_ne_zero`, `veblen_opow_eq_opow_iff`, `veblen_pos`, `veblen_right_strictMono`, `veblen_succ`, `veblen_veblen_eq_veblen_iff`, `veblen_veblen_of_lt`, `veblen_zero`, `veblen_zero_apply`, `veblen_zero_inj`, `veblen_zero_le_veblen_zero`, `veblen_zero_lt_veblen_zero`, `veblen_zero_strictMono`	128
Total	138

Ordinal

Definitions

Name	Category	Theorems
`epsilon` 📖	CompOp	16 math math: `epsilon_eq_deriv`, `epsilon_zero_lt_gamma`, `epsilon_zero_le_of_omega0_opow_le`, `lt_epsilon_zero`, `iterate_omega0_opow_lt_epsilon0`, `epsilon_succ_eq_nfp`, `epsilon0_lt_gamma`, `omega0_lt_epsilon`, `epsilon0_eq_nfp`, `epsilon_zero_eq_nfp`, `epsilon0_le_of_omega0_opow_le`, `epsilon_pos`, `iterate_omega0_opow_lt_epsilon_zero`, `natCast_lt_epsilon`, `lt_epsilon0`, `omega0_opow_epsilon`
`gamma` 📖	CompOp	26 math math: `gamma_le_gamma`, `gamma_zero_eq_nfp`, `epsilon_zero_lt_gamma`, `veblen_gamma_zero`, `gamma_inj`, `gamma0_le_of_veblen_le`, `lt_gamma0`, `iterate_veblen_lt_gamma0`, `invVeblen₂_gamma`, `gamma_pos`, `gamma_zero_le_of_veblen_le`, `strictMono_gamma`, `iterate_veblen_lt_gamma_zero`, `epsilon0_lt_gamma`, `isNormal_gamma`, `mem_range_gamma`, `omega0_lt_gamma`, `gamma0_eq_nfp`, `lt_gamma_zero`, `gamma_lt_gamma`, `invVeblen₁_lt_iff`, `invVeblen₁_eq_iff`, `natCast_lt_gamma`, `gamma_succ_eq_nfp`, `monotone_gamma`, `invVeblen₁_gamma`
`invVeblen₁` 📖	CompOp	18 math math: `invVeblen₂_eq_iff`, `le_invVeblen₂_iff`, `invVeblen₁_zero`, `invVeblen₂_le_iff`, `invVeblen₁_le`, `invVeblen₁_of_lt_opow`, `mem_range_veblen_iff_le_invVeblen₁`, `veblen_invVeblen₁_invVeblen₂`, `lt_veblen_iff_invVeblen₁_le`, `invVeblen₁_lt_iff`, `invVeblen₂_lt_iff`, `lt_invVeblen₂_iff`, `veblen_eq_opow_iff`, `invVeblen₁_veblen`, `lt_veblen_invVeblen₁`, `invVeblen₁_epsilon`, `invVeblen₁_eq_iff`, `invVeblen₁_gamma`
`invVeblen₂` 📖	CompOp	14 math math: `invVeblen₂_epsilon`, `invVeblen₂_eq_iff`, `le_invVeblen₂_iff`, `invVeblen₂_zero`, `invVeblen₂_le_iff`, `invVeblen₂_gamma`, `veblen_invVeblen₁_invVeblen₂`, `invVeblen₂_of_lt_opow`, `invVeblen₂_le`, `invVeblen₂_lt_iff`, `invVeblen₂_lt`, `lt_invVeblen₂_iff`, `veblen_eq_opow_iff`, `invVeblen₂_veblen`
`termΓ_` 📖	CompOp	—
`termΓ₀` 📖	CompOp	—
`termε_` 📖	CompOp	—
`termε₀` 📖	CompOp	—
`veblen` 📖	CompOp	50 math math: `invVeblen₂_eq_iff`, `le_invVeblen₂_iff`, `gamma_zero_eq_nfp`, `veblen_gamma_zero`, `veblen_eq_of_lt_invVeblen₁`, `invVeblen₂_le_iff`, `isNormal_veblen`, `lt_gamma0`, `veblen_zero_lt_veblen_zero`, `veblen_of_ne_zero`, `veblen_opow_eq_opow_iff`, `iterate_veblen_lt_gamma0`, `veblen_zero`, `cmp_veblen`, `veblen_inj`, `veblen_veblen_of_lt`, `veblen_zero_le_veblen_zero`, `isNormal_veblen_zero`, `mem_range_veblen_iff_le_invVeblen₁`, `veblen_eq_veblen_iff`, `veblen_invVeblen₁_invVeblen₂`, `iterate_veblen_lt_gamma_zero`, `veblen_le_veblen_iff`, `veblen_le_veblen_iff_right`, `mem_range_veblen`, `veblen_lt_veblen_veblen_iff`, `veblen_mem_range_opow`, `mem_range_gamma`, `gamma0_eq_nfp`, `lt_gamma_zero`, `opow_lt_veblen_opow_iff`, `lt_veblen_iff_invVeblen₁_le`, `veblen_lt_veblen_iff`, `lt_veblen`, `invVeblen₂_lt_iff`, `veblen_veblen_eq_veblen_iff`, `lt_invVeblen₂_iff`, `veblen_right_strictMono`, `veblen_succ`, `veblen_zero_apply`, `left_le_veblen`, `veblen_lt_veblen_iff_right`, `veblen_injective`, `lt_veblen_invVeblen₁`, `veblen_zero_inj`, `veblen_zero_strictMono`, `right_le_veblen`, `gamma_succ_eq_nfp`, `veblen_pos`, `veblen_left_monotone`
`veblenWith` 📖	CompOp	32 math math: `veblenWith_le_veblenWith_iff_right`, `IsNormal.veblenWith`, `veblenWith_zero_lt_veblenWith_zero`, `veblenWith_apply_eq_apply_iff`, `veblenWith_right_strictMono`, `veblenWith_zero_strictMono`, `veblenWith_veblenWith_of_lt`, `veblenWith_zero_inj`, `isNormal_veblenWith`, `veblenWith_lt_veblenWith_iff`, `left_le_veblenWith`, `veblenWith_veblenWith_eq_veblenWith_iff`, `veblenWith_lt_veblenWith_iff_right`, `veblenWith_inj`, `veblenWith_le_veblenWith_iff`, `cmp_veblenWith`, `veblenWith_lt_veblenWith_veblenWith_iff`, `veblenWith_succ`, `veblenWith_injective`, `veblenWith_zero`, `veblenWith_zero_le_veblenWith_zero`, `isNormal_veblenWith'`, `mem_range_veblenWith`, `veblenWith_eq_veblenWith_iff`, `veblenWith_of_ne_zero`, `veblenWith_pos`, `isNormal_veblenWith_zero`, `veblenWith_left_monotone`, `IsNormal.veblenWith_zero`, `veblenWith_mem_range`, `right_le_veblenWith`, `apply_lt_veblenWith_apply_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_lt_veblenWith_apply_iff` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `veblenWith`	—	`veblenWith_zero` `veblenWith_lt_veblenWith_veblenWith_iff` `zero_le` `canonicallyOrderedAdd`
`cmp_veblen` 📖	mathematical	—	`cmp` `Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `LinearOrder.toDecidableLT` `instLinearOrder` `veblen`	—	`cmp_veblenWith` `isNormal_opow` `one_lt_omega0`
`cmp_veblenWith` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`cmp` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `LinearOrder.toDecidableLT` `veblenWith`	—	`lt_trichotomy` `veblenWith_veblenWith_of_lt` `StrictMono.cmp_map_eq` `veblenWith_right_strictMono` `LT.lt.cmp_eq_lt` `cmp_self_eq_eq` `LT.lt.cmp_eq_gt`
`epsilon0_eq_nfp` 📖	mathematical	—	`epsilon` `Ordinal` `zero` `nfp` `instPow` `omega0`	—	`epsilon_zero_eq_nfp`
`epsilon0_le_of_omega0_opow_le` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instPow` `omega0`	`epsilon` `zero`	—	`epsilon_zero_le_of_omega0_opow_le`
`epsilon0_lt_gamma` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `epsilon` `zero` `gamma`	—	`epsilon_zero_lt_gamma`
`epsilon_eq_deriv` 📖	mathematical	—	`epsilon` `deriv` `Ordinal` `instPow` `omega0`	—	`epsilon.eq_1` `succ_zero` `veblen_succ` `veblen_zero`
`epsilon_pos` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero` `epsilon`	—	`veblen_pos`
`epsilon_succ_eq_nfp` 📖	mathematical	—	`epsilon` `Order.succ` `Ordinal` `PartialOrder.toPreorder` `partialOrder` `instSuccOrder` `nfp` `instPow` `omega0`	—	`epsilon_eq_deriv` `deriv_succ`
`epsilon_zero_eq_nfp` 📖	mathematical	—	`epsilon` `Ordinal` `zero` `nfp` `instPow` `omega0`	—	`epsilon_eq_deriv` `deriv_zero_right`
`epsilon_zero_le_of_omega0_opow_le` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instPow` `omega0`	`epsilon` `zero`	—	`epsilon_zero_eq_nfp` `nfp_le_fp` `opow_le_opow_iff_right` `one_lt_omega0` `zero_le` `canonicallyOrderedAdd`
`epsilon_zero_lt_gamma` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `epsilon` `zero` `gamma`	—	`LE.le.trans_lt'` `gamma_le_gamma` `zero_le` `canonicallyOrderedAdd` `Function.iterate_one` `veblen_zero` `opow_zero` `iterate_veblen_lt_gamma_zero`
`gamma0_eq_nfp` 📖	mathematical	—	`gamma` `Ordinal` `zero` `nfp` `veblen`	—	`gamma_zero_eq_nfp`
`gamma0_le_of_veblen_le` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `veblen` `zero`	`gamma`	—	`gamma_zero_le_of_veblen_le`
`gamma_inj` 📖	mathematical	—	`gamma`	—	`StrictMono.injective` `strictMono_gamma`
`gamma_le_gamma` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `gamma`	—	`StrictMono.le_iff_le` `strictMono_gamma`
`gamma_lt_gamma` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `gamma`	—	`StrictMono.lt_iff_lt` `strictMono_gamma`
`gamma_ne_zero` 📖	—	—	—	—	`LT.lt.ne'` `gamma_pos`
`gamma_pos` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero` `gamma`	—	`natCast_lt_gamma`
`gamma_succ_eq_nfp` 📖	mathematical	—	`gamma` `Order.succ` `Ordinal` `PartialOrder.toPreorder` `partialOrder` `instSuccOrder` `nfp` `veblen` `zero`	—	`deriv_succ`
`gamma_zero_eq_nfp` 📖	mathematical	—	`gamma` `Ordinal` `zero` `nfp` `veblen`	—	`deriv_zero_right`
`gamma_zero_le_of_veblen_le` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `veblen` `zero`	`gamma`	—	`gamma_zero_eq_nfp` `nfp_le_fp` `veblen_left_monotone` `zero_le` `canonicallyOrderedAdd`
`invVeblen₁_epsilon` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `epsilon`	`invVeblen₁` `one`	—	`invVeblen₁_veblen`
`invVeblen₁_eq_iff` 📖	mathematical	—	`invVeblen₁` `Ordinal` `zero` `Set` `Set.instMembership` `Set.range` `gamma`	—	`mem_range_gamma` `LE.le.antisymm'` `left_le_veblen` `veblen_eq_of_lt_invVeblen₁` `Ne.bot_lt` `Eq.trans_ne` `bot_eq_zero` `veblen_zero_apply` `veblen_invVeblen₁_invVeblen₂` `canonicallyOrderedAdd` `invVeblen₁_zero` `invVeblen₁_gamma`
`invVeblen₁_gamma` 📖	mathematical	—	`invVeblen₁` `gamma`	—	`veblen_gamma_zero` `invVeblen₁_veblen` `veblen_pos`
`invVeblen₁_le` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `invVeblen₁`	—	`csInf_le'` `LT.lt.ne'` `lt_veblen`
`invVeblen₁_lt_iff` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `invVeblen₁` `Set` `Set.instMembership` `Set.range` `gamma`	—	`LE.le.lt_iff_ne` `invVeblen₁_le` `invVeblen₁_eq_iff`
`invVeblen₁_of_lt_opow` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instPow` `omega0`	`invVeblen₁` `zero`	—	`nonpos_iff_eq_zero` `canonicallyOrderedAdd` `lt_veblen_iff_invVeblen₁_le` `veblen_zero`
`invVeblen₁_veblen` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `veblen`	`invVeblen₁`	—	`le_antisymm` `lt_veblen_iff_invVeblen₁_le` `veblen_lt_veblen_iff_right` `mem_range_veblen_iff_le_invVeblen₁` `eq_zero_or_pos` `canonicallyOrderedAdd` `veblen_zero` `veblen_zero_apply` `veblen_veblen_of_lt`
`invVeblen₁_zero` 📖	mathematical	—	`invVeblen₁` `Ordinal` `zero`	—	`invVeblen₁_of_lt_opow` `opow_zero` `instZeroLEOneClass` `instNeZeroOne`
`invVeblen₂_epsilon` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `epsilon`	`invVeblen₂`	—	`invVeblen₂_veblen` `one_ne_zero` `instNeZeroOne`
`invVeblen₂_eq_iff` 📖	mathematical	—	`invVeblen₂` `Ordinal` `instPow` `omega0` `veblen` `invVeblen₁`	—	`veblen_invVeblen₁_invVeblen₂`
`invVeblen₂_gamma` 📖	mathematical	—	`invVeblen₂` `gamma` `Ordinal` `zero`	—	`veblen_gamma_zero` `invVeblen₂_veblen` `gamma_ne_zero` `veblen_pos`
`invVeblen₂_le` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `invVeblen₂`	—	`eq_zero_or_pos` `canonicallyOrderedAdd` `invVeblen₂_le_iff` `veblen_zero` `le_refl` `veblen_zero_apply` `veblen_eq_of_lt_invVeblen₁` `LT.lt.le` `invVeblen₂_lt`
`invVeblen₂_le_iff` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `invVeblen₂` `instPow` `omega0` `veblen` `invVeblen₁`	—	`veblen_le_veblen_iff_right` `veblen_invVeblen₁_invVeblen₂`
`invVeblen₂_lt` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `invVeblen₂` `instPow` `omega0`	—	`invVeblen₂_lt_iff` `opow_lt_veblen_opow_iff` `lt_veblen_invVeblen₁`
`invVeblen₂_lt_iff` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `invVeblen₂` `instPow` `omega0` `veblen` `invVeblen₁`	—	`veblen_lt_veblen_iff_right` `veblen_invVeblen₁_invVeblen₂`
`invVeblen₂_of_lt_opow` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instPow` `omega0`	`invVeblen₂`	—	`invVeblen₂_eq_iff` `invVeblen₁_of_lt_opow` `veblen_zero_apply`
`invVeblen₂_veblen` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `veblen`	`invVeblen₂`	—	`invVeblen₂_eq_iff` `invVeblen₁_veblen` `veblen_zero_apply` `veblen_veblen_of_lt` `Ne.bot_lt`
`invVeblen₂_zero` 📖	mathematical	—	`invVeblen₂` `Ordinal` `zero`	—	`invVeblen₂_of_lt_opow` `opow_zero` `instZeroLEOneClass` `instNeZeroOne`
`isNormal_gamma` 📖	mathematical	—	`Order.IsNormal` `Ordinal` `instLinearOrder` `gamma`	—	`isNormal_deriv`
`isNormal_veblen` 📖	mathematical	—	`Order.IsNormal` `Ordinal` `instLinearOrder` `veblen`	—	`isNormal_veblenWith` `isNormal_opow` `one_lt_omega0`
`isNormal_veblenWith` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`veblenWith`	—	`eq_or_ne` `veblenWith_zero` `isNormal_veblenWith'`
`isNormal_veblenWith'` 📖	mathematical	—	`Order.IsNormal` `Ordinal` `instLinearOrder` `veblenWith`	—	`veblenWith_of_ne_zero` `isNormal_derivFamily` `small_Iio`
`isNormal_veblenWith_zero` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero`	`veblenWith`	—	`Order.isNormal_iff` `veblenWith_zero_strictMono` `veblenWith_of_ne_zero` `Order.IsSuccLimit.ne_bot` `derivFamily_zero` `nfpFamily_le` `veblenWith_zero` `canonicallyOrderedAdd` `bot_eq_zero'` `Order.IsSuccLimit.bot_lt` `Order.IsSuccLimit.succ_lt` `max_lt` `LE.le.trans` `StrictMono.monotone` `veblenWith_right_strictMono` `veblenWith_left_monotone` `le_max_right` `Order.le_succ` `veblenWith_veblenWith_of_lt` `Order.lt_succ_iff` `instNoMaxOrder` `le_max_left` `le_refl`
`isNormal_veblen_zero` 📖	mathematical	—	`Order.IsNormal` `Ordinal` `instLinearOrder` `veblen` `zero`	—	`isNormal_veblenWith_zero` `isNormal_opow` `one_lt_omega0` `opow_zero` `instZeroLEOneClass` `instNeZeroOne`
`iterate_omega0_opow_lt_epsilon0` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `Nat.iterate` `instPow` `omega0` `zero` `epsilon`	—	`iterate_omega0_opow_lt_epsilon_zero`
`iterate_omega0_opow_lt_epsilon_zero` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `Nat.iterate` `instPow` `omega0` `zero` `epsilon`	—	`epsilon_zero_eq_nfp` `iterate_lt_nfp` `Order.IsNormal.strictMono` `isNormal_opow` `one_lt_omega0` `opow_zero` `instZeroLEOneClass` `instNeZeroOne`
`iterate_veblen_lt_gamma0` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `Nat.iterate` `veblen` `zero` `gamma`	—	`iterate_veblen_lt_gamma_zero`
`iterate_veblen_lt_gamma_zero` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `Nat.iterate` `veblen` `zero` `gamma`	—	`gamma_zero_eq_nfp` `iterate_lt_nfp` `veblen_zero_strictMono` `veblen_zero` `opow_zero` `instZeroLEOneClass` `instNeZeroOne`
`le_invVeblen₂_iff` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `invVeblen₂` `veblen` `invVeblen₁` `instPow` `omega0`	—	`veblen_le_veblen_iff_right` `veblen_invVeblen₁_invVeblen₂`
`left_le_veblen` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `veblen`	—	`left_le_veblenWith` `isNormal_opow` `one_lt_omega0` `opow_zero` `instZeroLEOneClass` `instNeZeroOne`
`left_le_veblenWith` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero`	`Preorder.toLE` `veblenWith`	—	`LE.le.trans` `StrictMono.le_apply` `wellFoundedLT` `veblenWith_zero_strictMono` `StrictMono.monotone` `veblenWith_right_strictMono` `zero_le` `canonicallyOrderedAdd`
`lt_epsilon0` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `epsilon` `zero` `Nat.iterate` `instPow` `omega0`	—	`lt_epsilon_zero`
`lt_epsilon_zero` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `epsilon` `zero` `Nat.iterate` `instPow` `omega0`	—	`epsilon_zero_eq_nfp` `lt_nfp_iff`
`lt_gamma0` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `gamma` `zero` `Nat.iterate` `veblen`	—	`lt_gamma_zero`
`lt_gamma_zero` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `gamma` `zero` `Nat.iterate` `veblen`	—	`gamma_zero_eq_nfp` `lt_nfp_iff`
`lt_invVeblen₂_iff` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `invVeblen₂` `veblen` `invVeblen₁` `instPow` `omega0`	—	`veblen_lt_veblen_iff_right` `veblen_invVeblen₁_invVeblen₂`
`lt_veblen` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `veblen`	—	`eq_zero_or_pos` `canonicallyOrderedAdd` `veblen_zero` `opow_zero` `instZeroLEOneClass` `instNeZeroOne` `LE.le.trans_lt` `left_le_veblen`
`lt_veblen_iff_invVeblen₁_le` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `veblen` `Preorder.toLE` `invVeblen₁`	—	`lt_or_ge` `veblen_eq_of_lt_invVeblen₁` `LT.lt.trans_le` `lt_veblen_invVeblen₁` `veblen_left_monotone`
`lt_veblen_invVeblen₁` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `veblen` `invVeblen₁`	—	`LE.le.lt_of_ne'` `right_le_veblen` `csInf_mem` `wellFoundedLT` `LT.lt.ne'` `lt_veblen`
`mem_range_gamma` 📖	mathematical	—	`Ordinal` `Set` `Set.instMembership` `Set.range` `gamma` `veblen` `zero`	—	`mem_range_deriv` `isNormal_veblen_zero`
`mem_range_veblen` 📖	mathematical	—	`Ordinal` `Set` `Set.instMembership` `Set.range` `veblen`	—	`mem_range_veblenWith` `isNormal_opow` `one_lt_omega0`
`mem_range_veblenWith` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`Set` `Set.instMembership` `Set.range` `veblenWith`	—	`veblenWith_of_ne_zero` `mem_range_derivFamily` `small_Iio` `isNormal_veblenWith`
`mem_range_veblen_iff_le_invVeblen₁` 📖	mathematical	—	`Ordinal` `Set` `Set.instMembership` `Set.range` `veblen` `instPow` `omega0` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `invVeblen₁`	—	`lt_trichotomy` `veblen_opow_eq_opow_iff` `veblen_eq_of_lt_invVeblen₁` `LT.lt.le` `veblen_zero` `mem_range_veblen` `le_rfl` `LT.lt.ne'` `lt_veblen_invVeblen₁` `veblen_veblen_of_lt` `LT.lt.not_ge`
`monotone_gamma` 📖	mathematical	—	`Monotone` `Ordinal` `PartialOrder.toPreorder` `partialOrder` `gamma`	—	`Order.IsNormal.monotone` `isNormal_gamma`
`natCast_lt_epsilon` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `epsilon`	—	`LT.lt.trans` `nat_lt_omega0` `omega0_lt_epsilon`
`natCast_lt_gamma` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `AddMonoidWithOne.toNatCast` `addMonoidWithOne` `gamma`	—	`LT.lt.trans` `nat_lt_omega0` `omega0_lt_gamma`
`omega0_lt_epsilon` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `omega0` `epsilon`	—	`lt_of_lt_of_le` `Function.iterate_one` `opow_zero` `opow_one` `iterate_omega0_opow_lt_epsilon_zero` `StrictMono.monotone` `veblen_right_strictMono` `zero_le` `canonicallyOrderedAdd`
`omega0_lt_gamma` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `omega0` `gamma`	—	`LT.lt.trans` `omega0_lt_epsilon` `epsilon_zero_lt_gamma`
`omega0_opow_epsilon` 📖	mathematical	—	`Ordinal` `instPow` `omega0` `epsilon`	—	`epsilon_eq_deriv` `deriv_fp` `isNormal_opow` `one_lt_omega0`
`opow_lt_veblen_opow_iff` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instPow` `omega0` `veblen`	—	`apply_lt_veblenWith_apply_iff` `isNormal_opow` `one_lt_omega0`
`right_le_veblen` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `veblen`	—	`right_le_veblenWith` `isNormal_opow` `one_lt_omega0`
`right_le_veblenWith` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `veblenWith`	—	`StrictMono.le_apply` `wellFoundedLT` `veblenWith_right_strictMono`
`strictMono_gamma` 📖	mathematical	—	`StrictMono` `Ordinal` `PartialOrder.toPreorder` `partialOrder` `gamma`	—	`Order.IsNormal.strictMono` `isNormal_gamma`
`veblenWith_apply_eq_apply_iff` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`veblenWith`	—	`veblenWith_zero` `veblenWith_veblenWith_eq_veblenWith_iff` `zero_le` `canonicallyOrderedAdd`
`veblenWith_eq_self_of_le` 📖	—	`Order.IsNormal` `Ordinal` `instLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `veblenWith`	—	—	`LE.le.eq_or_lt` `veblenWith_veblenWith_of_lt`
`veblenWith_eq_veblenWith_iff` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`veblenWith` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder`	—	`cmp_eq_eq_iff` `cmp_veblenWith` `cmp.congr_simp` `cmp_self_eq_eq`
`veblenWith_inj` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`veblenWith`	—	`veblenWith_injective`
`veblenWith_injective` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`veblenWith`	—	`StrictMono.injective` `veblenWith_right_strictMono`
`veblenWith_le_veblenWith_iff` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `veblenWith` `Preorder.toLT`	—	`not_lt` `cmp_eq_gt_iff` `cmp_veblenWith` `cmp.congr_simp` `cmp_self_eq_eq`
`veblenWith_le_veblenWith_iff_right` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `veblenWith`	—	`StrictMono.le_iff_le` `veblenWith_right_strictMono`
`veblenWith_left_monotone` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`Monotone` `PartialOrder.toPreorder` `partialOrder` `veblenWith`	—	`monotone_iff_forall_lt` `veblenWith_veblenWith_of_lt` `StrictMono.monotone` `veblenWith_right_strictMono` `right_le_veblenWith`
`veblenWith_lt_veblenWith_iff` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `veblenWith`	—	`cmp_eq_lt_iff` `cmp_veblenWith` `cmp.congr_simp` `cmp_self_eq_eq`
`veblenWith_lt_veblenWith_iff_right` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `veblenWith`	—	`StrictMono.lt_iff_lt` `veblenWith_right_strictMono`
`veblenWith_lt_veblenWith_veblenWith_iff` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder`	`Preorder.toLT` `veblenWith`	—	`LE.le.lt_iff_ne'` `right_le_veblenWith` `veblenWith_veblenWith_eq_veblenWith_iff`
`veblenWith_mem_range` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`Set` `Set.instMembership` `Set.range` `veblenWith`	—	`eq_zero_or_pos` `canonicallyOrderedAdd` `veblenWith_zero` `veblenWith_veblenWith_of_lt`
`veblenWith_of_ne_zero` 📖	mathematical	—	`veblenWith` `derivFamily` `Set.Elem` `Ordinal` `Set.Iio` `PartialOrder.toPreorder` `partialOrder` `Set` `Set.instMembership`	—	`veblenWith.eq_1`
`veblenWith_pos` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero`	`veblenWith`	—	`veblenWith_zero` `LT.lt.trans_le` `Order.IsNormal.monotone` `zero_le` `canonicallyOrderedAdd` `eq_zero_or_pos` `veblenWith_veblenWith_of_lt`
`veblenWith_right_strictMono` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`StrictMono` `PartialOrder.toPreorder` `partialOrder` `veblenWith`	—	`Order.IsNormal.strictMono` `isNormal_veblenWith`
`veblenWith_succ` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder`	`veblenWith` `Order.succ` `PartialOrder.toPreorder` `partialOrder` `instSuccOrder` `deriv`	—	`deriv_eq_enumOrd` `isNormal_veblenWith` `veblenWith_of_ne_zero` `succ_ne_zero` `derivFamily_eq_enumOrd` `small_Iio` `Set.ext` `Set.mem_iInter` `Order.lt_succ` `instNoMaxOrder` `Order.lt_succ_iff_eq_or_lt` `Function.mem_fixedPoints_iff` `veblenWith_veblenWith_of_lt`
`veblenWith_veblenWith_eq_veblenWith_iff` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder`	`veblenWith`	—	—
`veblenWith_veblenWith_of_lt` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder`	`veblenWith`	—	`mem_range_veblenWith` `LT.lt.ne_bot`
`veblenWith_zero` 📖	mathematical	—	`veblenWith` `Ordinal` `zero`	—	`veblenWith.eq_1`
`veblenWith_zero_inj` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero`	`veblenWith`	—	`StrictMono.injective` `veblenWith_zero_strictMono`
`veblenWith_zero_le_veblenWith_zero` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero`	`Preorder.toLE` `veblenWith`	—	`StrictMono.le_iff_le` `veblenWith_zero_strictMono`
`veblenWith_zero_lt_veblenWith_zero` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero`	`veblenWith`	—	`StrictMono.lt_iff_lt` `veblenWith_zero_strictMono`
`veblenWith_zero_strictMono` 📖	mathematical	`Order.IsNormal` `Ordinal` `instLinearOrder` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero`	`StrictMono` `veblenWith`	—	`veblenWith_veblenWith_of_lt` `veblenWith_lt_veblenWith_iff_right` `veblenWith_pos`
`veblen_eq_of_lt_invVeblen₁` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `invVeblen₁`	`veblen`	—	`notMem_of_lt_csInf'`
`veblen_eq_opow_iff` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `veblen`	`instPow` `omega0` `invVeblen₁` `invVeblen₂`	—	`eq_zero_or_pos` `canonicallyOrderedAdd` `invVeblen₁_of_lt_opow` `veblen_zero` `invVeblen₂_of_lt_opow` `veblen_veblen_of_lt` `veblen_zero_apply` `one_lt_omega0` `invVeblen₁_veblen` `invVeblen₂_veblen` `LT.lt.ne'` `veblen_invVeblen₁_invVeblen₂`
`veblen_eq_self_of_le` 📖	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `veblen`	—	—	`veblenWith_eq_self_of_le` `isNormal_opow` `one_lt_omega0`
`veblen_eq_veblen_iff` 📖	mathematical	—	`veblen` `Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder`	—	`veblenWith_eq_veblenWith_iff` `isNormal_opow` `one_lt_omega0`
`veblen_gamma_zero` 📖	mathematical	—	`veblen` `gamma` `Ordinal` `zero`	—	`deriv_fp` `isNormal_veblen_zero`
`veblen_inj` 📖	mathematical	—	`veblen`	—	`veblen_injective`
`veblen_injective` 📖	mathematical	—	`Ordinal` `veblen`	—	`veblenWith_injective` `isNormal_opow` `one_lt_omega0`
`veblen_invVeblen₁_invVeblen₂` 📖	mathematical	—	`veblen` `invVeblen₁` `invVeblen₂` `Ordinal` `instPow` `omega0`	—	`mem_range_veblen_iff_le_invVeblen₁` `le_rfl`
`veblen_le_veblen_iff` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `veblen` `Preorder.toLT`	—	`veblenWith_le_veblenWith_iff` `isNormal_opow` `one_lt_omega0`
`veblen_le_veblen_iff_right` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `veblen`	—	`veblenWith_le_veblenWith_iff_right` `isNormal_opow` `one_lt_omega0`
`veblen_left_monotone` 📖	mathematical	—	`Monotone` `Ordinal` `PartialOrder.toPreorder` `partialOrder` `veblen`	—	`veblenWith_left_monotone` `isNormal_opow` `one_lt_omega0`
`veblen_lt_veblen_iff` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `veblen`	—	`veblenWith_lt_veblenWith_iff` `isNormal_opow` `one_lt_omega0`
`veblen_lt_veblen_iff_right` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `veblen`	—	`veblenWith_lt_veblenWith_iff_right` `isNormal_opow` `one_lt_omega0`
`veblen_lt_veblen_veblen_iff` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder`	`Preorder.toLT` `veblen`	—	`veblenWith_lt_veblenWith_veblenWith_iff` `isNormal_opow` `one_lt_omega0`
`veblen_mem_range_opow` 📖	mathematical	—	`Ordinal` `Set` `Set.instMembership` `Set.range` `instPow` `omega0` `veblen`	—	`veblenWith_mem_range` `isNormal_opow` `one_lt_omega0`
`veblen_of_ne_zero` 📖	mathematical	—	`veblen` `derivFamily` `Set.Elem` `Ordinal` `Set.Iio` `PartialOrder.toPreorder` `partialOrder` `Set` `Set.instMembership`	—	`veblenWith_of_ne_zero`
`veblen_opow_eq_opow_iff` 📖	mathematical	—	`veblen` `Ordinal` `instPow` `omega0`	—	`veblenWith_apply_eq_apply_iff` `isNormal_opow` `one_lt_omega0`
`veblen_pos` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero` `veblen`	—	`veblenWith_pos` `isNormal_opow` `one_lt_omega0` `opow_zero` `instZeroLEOneClass` `instNeZeroOne`
`veblen_right_strictMono` 📖	mathematical	—	`StrictMono` `Ordinal` `PartialOrder.toPreorder` `partialOrder` `veblen`	—	`veblenWith_right_strictMono` `isNormal_opow` `one_lt_omega0`
`veblen_succ` 📖	mathematical	—	`veblen` `Order.succ` `Ordinal` `PartialOrder.toPreorder` `partialOrder` `instSuccOrder` `deriv`	—	`veblenWith_succ` `isNormal_opow` `one_lt_omega0`
`veblen_veblen_eq_veblen_iff` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder`	`veblen`	—	`veblenWith_veblenWith_eq_veblenWith_iff` `isNormal_opow` `one_lt_omega0`
`veblen_veblen_of_lt` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder`	`veblen`	—	`veblenWith_veblenWith_of_lt` `isNormal_opow` `one_lt_omega0`
`veblen_zero` 📖	mathematical	—	`veblen` `Ordinal` `zero` `instPow` `omega0`	—	`veblen.eq_1` `veblenWith_zero`
`veblen_zero_apply` 📖	mathematical	—	`veblen` `Ordinal` `zero` `instPow` `omega0`	—	`veblen_zero`
`veblen_zero_inj` 📖	mathematical	—	`veblen` `Ordinal` `zero`	—	`StrictMono.injective` `veblen_zero_strictMono`
`veblen_zero_le_veblen_zero` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `veblen` `zero`	—	`StrictMono.le_iff_le` `veblen_zero_strictMono`
`veblen_zero_lt_veblen_zero` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `veblen` `zero`	—	`StrictMono.lt_iff_lt` `veblen_zero_strictMono`
`veblen_zero_strictMono` 📖	mathematical	—	`StrictMono` `Ordinal` `PartialOrder.toPreorder` `partialOrder` `veblen` `zero`	—	`veblenWith_zero_strictMono` `isNormal_opow` `one_lt_omega0` `opow_zero` `instZeroLEOneClass` `instNeZeroOne`

Ordinal.IsNormal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`veblenWith` 📖	mathematical	`Order.IsNormal` `Ordinal` `Ordinal.instLinearOrder`	`Ordinal.veblenWith`	—	`Ordinal.isNormal_veblenWith`
`veblenWith_zero` 📖	mathematical	`Order.IsNormal` `Ordinal` `Ordinal.instLinearOrder` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.zero`	`Ordinal.veblenWith`	—	`Ordinal.isNormal_veblenWith_zero`

---

← Back to Index