Notation

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

Statistics

Metric	Count
Definitions `NONote`, `below`, `cmp`, `instAdd`, `instInhabited`, `instLinearOrder`, `instMul`, `instPreorder`, `instRepr`, `instSub`, `instToString`, `instWellFoundedRelation`, `instZero`, `mk`, `oadd`, `ofNat`, `opow`, `recOn`, `repr`, `ONote`, `FundamentalSequenceProp`, `NF`, `NFBelow`, `TopBelow`, `add`, `addAux`, `cmp`, `decidableNF`, `decidableTopBelow`, `fastGrowing`, `fastGrowingε₀`, `fundamentalSequence`, `instAdd`, `instInhabited`, `instMul`, `instMulZeroClass`, `instOne`, `instPow`, `instPreorder`, `instRepr`, `instSub`, `instToString`, `instWellFoundedRelation`, `instZero`, `mul`, `mulNat`, `nat`, `ofNat`, `omega`, `opow`, `opowAux`, `opowAux2`, `repr`, `repr'`, `scale`, `split`, `split'`, `sub`, `toString`, `instDecidableEqNONote`, `instDecidableEqONote`, `decEq`	62
Theorems `NF`, `cmp_compares`, `instWellFoundedLT`, `lt_wf`, `repr_add`, `repr_mul`, `repr_opow`, `repr_sub`, `below_of_lt`, `below_of_lt'`, `fst`, `oadd`, `oadd_zero`, `of_dvd_omega0`, `of_dvd_omega0_opow`, `out`, `snd`, `snd'`, `zero`, `zero_of_zero`, `fst`, `lt`, `mono`, `oadd`, `repr_lt`, `snd`, `NFBelow_zero`, `add_nf`, `add_nfBelow`, `cmp_compares`, `eq_of_cmp_eq`, `fastGrowing_def`, `fastGrowing_limit`, `fastGrowing_one`, `fastGrowing_succ`, `fastGrowing_two`, `fastGrowing_zero`, `fastGrowing_zero'`, `fastGrowingε₀_one`, `fastGrowingε₀_two`, `fastGrowingε₀_zero`, `fundamentalSequenceProp_inl_none`, `fundamentalSequenceProp_inl_some`, `fundamentalSequenceProp_inr`, `fundamentalSequence_has_prop`, `le_def`, `lt_def`, `mulNat_eq_mul`, `mul_nf`, `nfBelow_iff_topBelow`, `nfBelow_ofNat`, `nf_mulNat`, `nf_ofNat`, `nf_one`, `nf_opow`, `nf_opowAux`, `nf_repr_split`, `nf_repr_split'`, `nf_scale`, `oadd_add`, `oadd_lt_oadd_1`, `oadd_lt_oadd_2`, `oadd_lt_oadd_3`, `oadd_mul`, `oadd_mul_nfBelow`, `oadd_pos`, `ofNat_one`, `ofNat_succ`, `ofNat_zero`, `omega0_le_oadd`, `opow_def`, `repr_add`, `repr_inj`, `repr_le_repr`, `repr_lt_repr`, `repr_mul`, `repr_ofNat`, `repr_one`, `repr_opow`, `repr_opow_aux₁`, `repr_opow_aux₂`, `repr_scale`, `repr_sub`, `repr_zero`, `scale_eq_mul`, `scale_opowAux`, `split_add_lt`, `split_dvd`, `split_eq_scale_split'`, `sub_nf`, `sub_nfBelow`, `zero_add`, `zero_def`, `zero_lt_one`	94
Total	156

NONote

Definitions

Name	Category	Theorems
`below` 📖	MathDef	—
`cmp` 📖	CompOp	1 math math: `cmp_compares`
`instAdd` 📖	CompOp	1 math math: `repr_add`
`instInhabited` 📖	CompOp	—
`instLinearOrder` 📖	CompOp	—
`instMul` 📖	CompOp	1 math math: `repr_mul`
`instPreorder` 📖	CompOp	3 math math: `cmp_compares`, `lt_wf`, `instWellFoundedLT`
`instRepr` 📖	CompOp	—
`instSub` 📖	CompOp	1 math math: `repr_sub`
`instToString` 📖	CompOp	—
`instWellFoundedRelation` 📖	CompOp	—
`instZero` 📖	CompOp	—
`mk` 📖	CompOp	—
`oadd` 📖	CompOp	—
`ofNat` 📖	CompOp	—
`opow` 📖	CompOp	1 math math: `repr_opow`
`recOn` 📖	CompOp	—
`repr` 📖	CompOp	4 math math: `repr_add`, `repr_opow`, `repr_sub`, `repr_mul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`NF` 📖	mathematical	—	`ONote.NF` `ONote`	—	—
`cmp_compares` 📖	mathematical	—	`Ordering.Compares` `NONote` `Preorder.toLT` `instPreorder` `cmp`	—	`ONote.cmp_compares`
`instWellFoundedLT` 📖	mathematical	—	`WellFoundedLT` `NONote` `Preorder.toLT` `instPreorder`	—	`lt_wf`
`lt_wf` 📖	mathematical	—	`NONote` `Preorder.toLT` `instPreorder`	—	`Ordinal.lt_wf`
`repr_add` 📖	mathematical	—	`repr` `NONote` `instAdd` `Ordinal` `Ordinal.add`	—	`ONote.repr_add` `NF`
`repr_mul` 📖	mathematical	—	`repr` `NONote` `instMul` `Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Ordinal.monoidWithZero`	—	`ONote.repr_mul` `NF`
`repr_opow` 📖	mathematical	—	`repr` `opow` `Ordinal` `Ordinal.instPow`	—	`ONote.repr_opow` `NF`
`repr_sub` 📖	mathematical	—	`repr` `NONote` `instSub` `Ordinal` `Ordinal.sub`	—	`ONote.repr_sub` `NF`

ONote

Definitions

Name	Category	Theorems
`FundamentalSequenceProp` 📖	MathDef	5 math math: `fundamentalSequenceProp_inl_none`, `fundamentalSequenceProp_inl_some`, `fundamentalSequenceProp_inr`, `fastGrowing_def`, `fundamentalSequence_has_prop`
`NF` 📖	CompData	21 math math: `nfBelow_iff_topBelow`, `nf_repr_split'`, `NF.snd`, `nf_opow`, `NF.oadd`, `NF.oadd_zero`, `sub_nf`, `fundamentalSequenceProp_inl_some`, `nf_ofNat`, `NF.fst`, `nf_one`, `mul_nf`, `fundamentalSequenceProp_inr`, `nf_scale`, `nf_opowAux`, `nf_repr_split`, `NFBelow.fst`, `NONote.NF`, `nf_mulNat`, `add_nf`, `NF.zero`
`NFBelow` 📖	CompData	7 math math: `nfBelow_iff_topBelow`, `NFBelow_zero`, `NF.out`, `NF.below_of_lt'`, `NF.below_of_lt`, `NF.snd'`, `nfBelow_ofNat`
`TopBelow` 📖	MathDef	1 math math: `nfBelow_iff_topBelow`
`add` 📖	CompOp	—
`addAux` 📖	CompOp	1 math math: `oadd_add`
`cmp` 📖	CompOp	1 math math: `cmp_compares`
`decidableNF` 📖	CompOp	—
`decidableTopBelow` 📖	CompOp	—
`fastGrowing` 📖	CompOp	7 math math: `fastGrowing_limit`, `fastGrowing_succ`, `fastGrowing_one`, `fastGrowing_zero`, `fastGrowing_zero'`, `fastGrowing_def`, `fastGrowing_two`
`fastGrowingε₀` 📖	CompOp	3 math math: `fastGrowingε₀_zero`, `fastGrowingε₀_two`, `fastGrowingε₀_one`
`fundamentalSequence` 📖	CompOp	1 math math: `fundamentalSequence_has_prop`
`instAdd` 📖	CompOp	6 math math: `zero_add`, `add_nfBelow`, `oadd_add`, `repr_add`, `oadd_mul`, `add_nf`
`instInhabited` 📖	CompOp	—
`instMul` 📖	CompOp	7 math math: `repr_mul`, `oadd_mul_nfBelow`, `mulNat_eq_mul`, `mul_nf`, `repr_opow_aux₂`, `scale_eq_mul`, `oadd_mul`
`instMulZeroClass` 📖	CompOp	—
`instOne` 📖	CompOp	6 math math: `repr_one`, `ofNat_one`, `zero_lt_one`, `split_eq_scale_split'`, `nf_one`, `fastGrowing_one`
`instPow` 📖	CompOp	3 math math: `nf_opow`, `repr_opow`, `opow_def`
`instPreorder` 📖	CompOp	7 math math: `cmp_compares`, `lt_def`, `zero_lt_one`, `le_def`, `fundamentalSequenceProp_inr`, `oadd_lt_oadd_2`, `oadd_pos`
`instRepr` 📖	CompOp	—
`instSub` 📖	CompOp	3 math math: `sub_nf`, `sub_nfBelow`, `repr_sub`
`instToString` 📖	CompOp	—
`instWellFoundedRelation` 📖	CompOp	—
`instZero` 📖	CompOp	16 math math: `ofNat_succ`, `NFBelow_zero`, `zero_add`, `repr_zero`, `fundamentalSequenceProp_inl_none`, `zero_lt_one`, `NF.oadd_zero`, `ofNat_zero`, `repr_opow_aux₂`, `scale_eq_mul`, `fastGrowing_zero`, `scale_opowAux`, `oadd_pos`, `zero_def`, `oadd_mul`, `NF.zero`
`mul` 📖	CompOp	—
`mulNat` 📖	CompOp	2 math math: `mulNat_eq_mul`, `nf_mulNat`
`nat` 📖	CompOp	1 math math: `fastGrowing_two`
`ofNat` 📖	CompOp	8 math math: `ofNat_succ`, `ofNat_one`, `ofNat_zero`, `mulNat_eq_mul`, `nf_ofNat`, `repr_ofNat`, `repr_opow_aux₂`, `nfBelow_ofNat`
`omega` 📖	CompOp	—
`opow` 📖	CompOp	—
`opowAux` 📖	CompOp	3 math math: `repr_opow_aux₂`, `scale_opowAux`, `nf_opowAux`
`opowAux2` 📖	CompOp	1 math math: `opow_def`
`repr` 📖	CompOp	27 math math: `nfBelow_iff_topBelow`, `repr_one`, `nf_repr_split'`, `repr_mul`, `split_dvd`, `lt_def`, `oadd_mul_nfBelow`, `NFBelow.lt`, `repr_add`, `repr_scale`, `repr_zero`, `omega0_le_oadd`, `le_def`, `split_add_lt`, `repr_opow`, `repr_inj`, `fundamentalSequenceProp_inl_some`, `repr_le_repr`, `fundamentalSequenceProp_inr`, `repr_lt_repr`, `repr_ofNat`, `scale_opowAux`, `NFBelow.snd`, `nf_repr_split`, `NF.snd'`, `repr_sub`, `NFBelow.repr_lt`
`repr'` 📖	CompOp	—
`scale` 📖	CompOp	4 math math: `repr_scale`, `split_eq_scale_split'`, `scale_eq_mul`, `nf_scale`
`split` 📖	CompOp	2 math math: `split_eq_scale_split'`, `opow_def`
`split'` 📖	CompOp	—
`sub` 📖	CompOp	—
`toString` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`NFBelow_zero` 📖	mathematical	—	`NFBelow` `Ordinal` `Ordinal.zero` `ONote` `instZero`	—	`not_le_of_gt` `NFBelow.lt` `zero_le` `Ordinal.canonicallyOrderedAdd`
`add_nf` 📖	mathematical	—	`NF` `ONote` `instAdd`	—	`le_total` `add_nfBelow` `NFBelow.mono`
`add_nfBelow` 📖	mathematical	`NFBelow`	`ONote` `instAdd`	—	`NFBelow.mono` `le_of_lt` `NFBelow.lt` `NFBelow.snd` `NFBelow.oadd` `NFBelow.fst` `cmp_compares` `NF.below_of_lt`
`cmp_compares` 📖	mathematical	—	`Ordering.Compares` `ONote` `Preorder.toLT` `instPreorder` `cmp`	—	`oadd_pos` `cmp.eq_4` `NF.fst` `oadd_lt_oadd_1` `not_lt` `ite_eq_iff` `cmpUsing.eq_1` `oadd_lt_oadd_2` `NF.snd` `oadd_lt_oadd_3` `LE.le.eq_of_not_lt`
`eq_of_cmp_eq` 📖	—	`cmp`	—	—	`le_antisymm_iff` `not_lt` `cmpUsing_eq_eq` `cmp.eq_1`
`fastGrowing_def` 📖	mathematical	`fundamentalSequence`	`fastGrowing` `ONote` `FundamentalSequenceProp` `fundamentalSequence_has_prop` `Nat.iterate`	—	`fundamentalSequence_has_prop` `fastGrowing.eq_1`
`fastGrowing_limit` 📖	mathematical	`fundamentalSequence` `ONote`	`fastGrowing`	—	`fundamentalSequence_has_prop` `fastGrowing_def`
`fastGrowing_one` 📖	mathematical	—	`fastGrowing` `ONote` `instOne`	—	`fastGrowing_succ` `Nat.instAtLeastTwoHAddOfNat` `two_mul` `fastGrowing_zero` `add_zero` `Function.iterate_succ'`
`fastGrowing_succ` 📖	mathematical	`fundamentalSequence` `ONote`	`fastGrowing` `Nat.iterate`	—	`fundamentalSequence_has_prop` `fastGrowing_def`
`fastGrowing_two` 📖	mathematical	—	`fastGrowing` `ONote` `nat` `Monoid.toNatPow` `Nat.instMonoid`	—	`fastGrowing_succ` `fastGrowing_one` `mul_left_iterate`
`fastGrowing_zero` 📖	mathematical	—	`fastGrowing` `ONote` `instZero`	—	`fastGrowing_zero'`
`fastGrowing_zero'` 📖	mathematical	`fundamentalSequence` `ONote`	`fastGrowing`	—	`fundamentalSequence_has_prop` `fastGrowing_def`
`fastGrowingε₀_one` 📖	mathematical	—	`fastGrowingε₀`	—	`Function.iterate_one` `fastGrowing_one` `mul_one`
`fastGrowingε₀_two` 📖	mathematical	—	`fastGrowingε₀`	—	`Function.iterate_one` `fastGrowing_limit` `fastGrowing_succ` `fastGrowing_two` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Meta.NormNum.IsNatPowT.trans`
`fastGrowingε₀_zero` 📖	mathematical	—	`fastGrowingε₀`	—	`fastGrowing_zero` `zero_add`
`fundamentalSequenceProp_inl_none` 📖	mathematical	—	`FundamentalSequenceProp` `ONote` `instZero`	—	—
`fundamentalSequenceProp_inl_some` 📖	mathematical	—	`FundamentalSequenceProp` `ONote` `repr` `Order.succ` `Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.instSuccOrder` `NF`	—	—
`fundamentalSequenceProp_inr` 📖	mathematical	—	`FundamentalSequenceProp` `ONote` `Order.IsSuccLimit` `Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder` `repr` `Preorder.toLT` `instPreorder` `NF`	—	—
`fundamentalSequence_has_prop` 📖	mathematical	—	`FundamentalSequenceProp` `fundamentalSequence`	—	`fundamentalSequence.eq_2` `PNat.natPred_add_one` `FundamentalSequenceProp.eq_1` `Ordinal.opow_zero` `Nat.cast_succ` `Nat.cast_zero` `zero_add` `mul_one` `add_zero` `Ordinal.succ_zero` `Nat.succPNat_coe` `mul_add_one` `Ordinal.leftDistribClass` `NF.oadd_zero` `NF.zero` `FundamentalSequenceProp.eq_2` `Ordinal.opow_succ` `Ordinal.instAddLeftStrictMono` `Ordinal.instAddLeftReflectLT` `Ordinal.opow_pos` `Ordinal.omega0_pos` `Ordinal.isSuccLimit_mul` `Ordinal.isSuccLimit_omega0` `Ordinal.mul_succ` `Ordinal.natCast_succ` `mul_lt_mul_of_pos_left` `Ordinal.instPosMulStrictMono` `Ordinal.nat_lt_omega0` `NF.fst` `Ordinal.isSuccLimit_add` `NF.oadd` `NF.below_of_lt'` `repr.eq_2` `zero_def` `repr.eq_1` `Ordinal.opow_lt_opow_iff_right` `Ordinal.one_lt_omega0` `FundamentalSequenceProp.eq_3` `Ordinal.isSuccLimit_opow` `PNat.one_coe` `Nat.cast_one` `Ordinal.add_succ` `NFBelow.repr_lt` `NF.snd'` `LT.lt.trans` `Order.lt_succ` `Ordinal.instNoMaxOrder` `NF.snd` `oadd_lt_oadd_3` `lt_trans`
`le_def` 📖	mathematical	—	`ONote` `Preorder.toLE` `instPreorder` `Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder` `repr`	—	—
`lt_def` 📖	mathematical	—	`ONote` `Preorder.toLT` `instPreorder` `Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder` `repr`	—	—
`mulNat_eq_mul` 📖	mathematical	—	`mulNat` `ONote` `instMul` `ofNat`	—	—
`mul_nf` 📖	mathematical	—	`NF` `ONote` `instMul`	—	`NF.zero` `oadd_mul_nfBelow`
`nfBelow_iff_topBelow` 📖	mathematical	—	`NFBelow` `repr` `NF` `TopBelow`	—	`Ordering.Compares.eq_lt` `cmp_compares` `NFBelow.fst` `NFBelow.lt` `NF.below_of_lt` `NF.fst`
`nfBelow_ofNat` 📖	mathematical	—	`NFBelow` `ofNat` `Ordinal` `Ordinal.one`	—	`NFBelow.oadd` `NF.zero` `zero_lt_one` `Ordinal.instZeroLEOneClass` `Ordinal.instNeZeroOne`
`nf_mulNat` 📖	mathematical	—	`NF` `mulNat`	—	`mulNat_eq_mul` `mul_nf` `nf_ofNat`
`nf_ofNat` 📖	mathematical	—	`NF` `ofNat`	—	`nfBelow_ofNat`
`nf_one` 📖	mathematical	—	`NF` `ONote` `instOne`	—	`ofNat_one` `nf_ofNat`
`nf_opow` 📖	mathematical	—	`NF` `ONote` `instPow`	—	`nf_repr_split` `NF.oadd_zero` `nf_repr_split'` `split_eq_scale_split'` `mulNat_eq_mul` `NF.fst` `mul_nf` `nf_scale` `nf_one` `add_nf` `nf_ofNat` `nf_opowAux`
`nf_opowAux` 📖	mathematical	—	`NF` `opowAux`	—	—
`nf_repr_split` 📖	mathematical	`split` `ONote`	`NF` `repr` `Ordinal` `Ordinal.add` `AddMonoidWithOne.toNatCast` `Ordinal.addMonoidWithOne`	—	`nf_repr_split'` `split_eq_scale_split'` `repr_scale` `nf_one` `repr_one` `Nat.cast_one` `Ordinal.opow_one` `nf_scale`
`nf_repr_split'` 📖	mathematical	`split'` `ONote`	`NF` `repr` `Ordinal` `Ordinal.add` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Ordinal.monoidWithZero` `Ordinal.omega0` `AddMonoidWithOne.toNatCast` `Ordinal.addMonoidWithOne`	—	`MulZeroClass.mul_zero` `Nat.cast_zero` `add_zero` `Ordinal.opow_zero` `one_mul` `NF.zero_of_zero` `zero_add` `NF.snd` `NF.fst` `NF.zero` `Ordinal.opow_add` `Ordinal.add_sub_cancel_of_le` `Ordinal.one_le_iff_ne_zero` `NF.oadd` `sub_nf` `nf_one` `repr_sub` `repr_one` `Nat.cast_one` `NF.below_of_lt'` `mul_lt_mul_iff_right₀` `Ordinal.instPosMulStrictMono` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `Ordinal.omega0_pos` `LE.le.trans_lt` `le_self_add` `Ordinal.canonicallyOrderedAdd` `Ordinal.opow_one` `NFBelow.repr_lt` `NF.snd'` `mul_assoc` `mul_add` `Ordinal.leftDistribClass` `add_assoc`
`nf_scale` 📖	mathematical	—	`NF` `scale`	—	`scale_eq_mul` `mul_nf` `NF.oadd_zero`
`oadd_add` 📖	mathematical	—	`ONote` `instAdd` `oadd` `addAux`	—	—
`oadd_lt_oadd_1` 📖	mathematical	`ONote` `Preorder.toLT` `instPreorder`	`oadd`	—	`lt_of_lt_of_le` `NFBelow.repr_lt` `NF.below_of_lt` `omega0_le_oadd`
`oadd_lt_oadd_2` 📖	mathematical	`PNat.val`	`ONote` `Preorder.toLT` `instPreorder` `oadd`	—	`LT.lt.trans_le` `add_lt_add_right` `Ordinal.instAddLeftStrictMono` `NFBelow.repr_lt` `NF.snd'` `le_trans` `Ordinal.mul_succ` `mul_le_mul_iff_right₀` `PosMulStrictMono.toPosMulMono` `Ordinal.instPosMulStrictMono` `PosMulStrictMono.toPosMulReflectLE` `Ordinal.opow_pos` `Ordinal.omega0_pos` `Order.succ_le_iff` `Ordinal.instNoMaxOrder` `Nat.cast_lt` `Ordinal.instAddLeftMono` `Ordinal.instZeroLEOneClass` `Ordinal.instCharZero` `le_self_add` `Ordinal.canonicallyOrderedAdd`
`oadd_lt_oadd_3` 📖	mathematical	`ONote` `Preorder.toLT` `instPreorder`	`oadd`	—	`lt_def` `repr.eq_def` `add_lt_add_right` `Ordinal.instAddLeftStrictMono` `repr_lt_repr`
`oadd_mul` 📖	mathematical	—	`ONote` `instMul` `oadd` `instZero` `instDecidableEqONote` `PNat` `instMulPNat` `instAdd`	—	—
`oadd_mul_nfBelow` 📖	mathematical	`NFBelow` `oadd`	`ONote` `instMul` `Ordinal` `Ordinal.add` `repr`	—	`NFBelow.snd` `NFBelow.oadd` `NFBelow.fst` `Ordinal.instAddLeftStrictMono` `Ordinal.instAddLeftReflectLT` `add_zero` `add_lt_add_iff_left` `lt_of_le_of_lt` `zero_le` `Ordinal.canonicallyOrderedAdd` `NFBelow.lt` `add_nf` `repr_add`
`oadd_pos` 📖	mathematical	—	`ONote` `Preorder.toLT` `instPreorder` `instZero` `oadd`	—	`lt_of_lt_of_le` `Ordinal.opow_pos` `Ordinal.omega0_pos` `omega0_le_oadd`
`ofNat_one` 📖	mathematical	—	`ofNat` `ONote` `instOne`	—	—
`ofNat_succ` 📖	mathematical	—	`ofNat` `oadd` `ONote` `instZero` `Nat.succPNat`	—	—
`ofNat_zero` 📖	mathematical	—	`ofNat` `ONote` `instZero`	—	—
`omega0_le_oadd` 📖	mathematical	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.instPow` `Ordinal.omega0` `repr` `oadd`	—	`le_trans` `zero_add` `Nat.cast_one` `mul_one` `mul_le_mul_iff_right₀` `PosMulStrictMono.toPosMulMono` `Ordinal.instPosMulStrictMono` `PosMulStrictMono.toPosMulReflectLE` `Ordinal.opow_pos` `Ordinal.omega0_pos` `Nat.cast_le` `Ordinal.instAddLeftMono` `Ordinal.instZeroLEOneClass` `Ordinal.instCharZero` `le_self_add` `Ordinal.canonicallyOrderedAdd`
`opow_def` 📖	mathematical	—	`ONote` `instPow` `opowAux2` `split`	—	—
`repr_add` 📖	mathematical	—	`repr` `ONote` `instAdd` `Ordinal` `Ordinal.add`	—	`zero_add` `NF.snd` `add_nf` `add_assoc` `NF.fst` `cmp_compares` `Ordinal.add_absorp` `NFBelow.repr_lt` `NF.below_of_lt` `Ordinal.opow_zero` `lt_of_le_of_lt` `le_self_add` `Ordinal.canonicallyOrderedAdd` `repr.eq_def` `Nat.cast_one` `mul_one` `mul_le_mul_iff_right₀` `PosMulStrictMono.toPosMulMono` `Ordinal.instPosMulStrictMono` `PosMulStrictMono.toPosMulReflectLE` `Ordinal.opow_pos` `Ordinal.omega0_pos` `Nat.cast_le` `Ordinal.instAddLeftMono` `Ordinal.instZeroLEOneClass` `Ordinal.instCharZero` `PNat.pos` `Nat.cast_add` `mul_add` `Ordinal.leftDistribClass`
`repr_inj` 📖	mathematical	—	`repr`	—	`cmp_compares` `ne_of_lt` `ne_of_gt`
`repr_le_repr` 📖	mathematical	`ONote` `Preorder.toLE` `instPreorder`	`Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder` `repr`	—	`le_def`
`repr_lt_repr` 📖	mathematical	`ONote` `Preorder.toLT` `instPreorder`	`Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder` `repr`	—	`lt_def`
`repr_mul` 📖	mathematical	—	`repr` `ONote` `instMul` `Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Ordinal.monoidWithZero`	—	`MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `NF.snd` `Ordinal.add_absorp` `NFBelow.repr_lt` `NF.snd'` `zero_add` `Nat.cast_one` `mul_one` `mul_le_mul_iff_right₀` `PosMulStrictMono.toPosMulMono` `Ordinal.instPosMulStrictMono` `PosMulStrictMono.toPosMulReflectLE` `Ordinal.opow_pos` `Ordinal.omega0_pos` `Nat.cast_le` `Ordinal.instAddLeftMono` `Ordinal.instZeroLEOneClass` `Ordinal.instCharZero` `PNat.ne_zero` `Ordinal.natCast_mul` `Ordinal.opow_zero` `one_mul` `NF.zero_of_zero` `add_zero` `Ordinal.natCast_succ` `Ordinal.add_mul_succ` `mul_assoc` `repr_add` `NF.fst` `Ordinal.opow_add` `mul_add` `Ordinal.leftDistribClass` `NF.zero` `Ordinal.add_mul_of_isSuccLimit` `Ordinal.isSuccLimit_opow_left` `Ordinal.isSuccLimit_omega0` `Ordinal.mul_omega0_dvd` `Nat.cast_pos'` `Ordinal.instNeZeroOne` `PNat.pos` `Ordinal.nat_lt_omega0` `Ordinal.opow_one` `Ordinal.opow_dvd_opow` `Ordinal.one_le_iff_ne_zero`
`repr_ofNat` 📖	mathematical	—	`repr` `ofNat` `Ordinal` `AddMonoidWithOne.toNatCast` `Ordinal.addMonoidWithOne`	—	`Nat.cast_zero` `Ordinal.opow_zero` `Nat.cast_add` `Nat.cast_one` `one_mul` `add_zero`
`repr_one` 📖	mathematical	—	`repr` `ONote` `instOne` `Ordinal` `AddMonoidWithOne.toNatCast` `Ordinal.addMonoidWithOne`	—	`repr_ofNat`
`repr_opow` 📖	mathematical	—	`repr` `ONote` `instPow` `Ordinal` `Ordinal.instPow`	—	`nf_repr_split` `repr_one` `Nat.cast_one` `Nat.cast_zero` `add_zero` `Ordinal.opow_zero` `Ordinal.zero_opow` `nf_repr_split'` `zero_add` `Ordinal.one_opow` `Nat.cast_succ` `Ordinal.opow_add` `Ordinal.opow_mul` `Ordinal.opow_omega0` `Ordinal.instNoMaxOrder` `Ordinal.instAddLeftMono` `Ordinal.instZeroLEOneClass` `Ordinal.instCharZero` `Ordinal.lt_omega0` `Ordinal.add_one_eq_succ` `Ordinal.natCast_pow` `Nat.cast_add` `Ordinal.opow_natCast` `NF.of_dvd_omega0` `split_dvd` `split_add_lt` `repr_add` `NF.snd` `nf_ofNat` `repr_ofNat` `split_eq_scale_split'` `repr_mul` `NF.fst` `nf_scale` `nf_one` `repr_scale` `Ordinal.opow_one` `mul_one` `add_assoc` `repr_opow_aux₁` `add_nf` `mulNat_eq_mul` `mul_nf` `nf_opowAux` `mul_assoc` `Ordinal.opow_succ` `scale_opowAux` `mul_add` `Ordinal.leftDistribClass` `pow_succ` `repr_opow_aux₂`
`repr_opow_aux₁` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.instPow` `Ordinal.omega0` `repr`	`Ordinal.add` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Ordinal.monoidWithZero` `AddMonoidWithOne.toNatCast` `Ordinal.addMonoidWithOne` `PNat.val`	—	`NF.oadd` `NF.below_of_lt'` `omega0_le_oadd` `le_antisymm` `Ordinal.opow_le_of_isSuccLimit` `LT.lt.ne'` `LT.lt.trans_le` `Ordinal.opow_pos` `Ordinal.omega0_pos` `repr.eq_2` `Ordinal.isSuccLimit_omega0` `NFBelow.repr_lt` `NF.below_of_lt` `Order.lt_succ` `Ordinal.instNoMaxOrder` `LE.le.trans` `Ordinal.opow_le_opow_left` `LT.lt.le` `Ordinal.opow_mul` `le_or_gt` `le_imp_le_of_le_of_le` `Ordinal.opow_le_opow` `le_refl` `mul_le_mul_right` `Ordinal.mulLeftMono` `Order.le_succ` `Ordinal.add_one_eq_succ` `Ordinal.add_mul_succ` `Ordinal.one_add_of_omega0_le` `Order.succ_le_iff` `mul_lt_mul_of_pos_left` `Ordinal.instPosMulStrictMono` `Order.IsSuccLimit.succ_lt` `lt_of_le_of_ne'` `zero_le` `Ordinal.canonicallyOrderedAdd` `le_of_lt` `Ordinal.principal_mul_omega0` `one_mul` `mul_le_mul_left` `Ordinal.mulRightMono` `Ordinal.one_le_iff_ne_zero`
`repr_opow_aux₂` 📖	mathematical	`Ordinal` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `Ordinal.monoidWithZero` `Ordinal.omega0` `repr` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.add` `AddMonoidWithOne.toNatCast` `Ordinal.addMonoidWithOne` `Ordinal.instPow`	`opowAux` `ONote` `instZero` `instMul` `oadd` `ofNat` `Order.succ` `Ordinal.instSuccOrder` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `PNat.val`	—	`Nat.cast_zero` `Ordinal.succ_zero` `Ordinal.opow_one` `instIsEmptyFalse` `Ordinal.opow_zero` `one_mul` `add_zero` `Nat.cast_add` `Nat.cast_one` `MulZeroClass.mul_zero` `opowAux.eq_1` `opowAux.eq_3` `mulNat_eq_mul` `repr_add` `nf_scale` `mul_nf` `nf_ofNat` `NF.oadd` `NF.below_of_lt'` `lt_of_le_of_lt` `le_self_add` `Ordinal.canonicallyOrderedAdd` `nf_opowAux` `NF.zero` `repr_scale` `repr_mul` `repr_ofNat` `Ordinal.opow_mul` `oadd_pos` `Ordinal.opow_pos` `Ordinal.omega0_pos` `mul_one` `lt_of_lt_of_le` `Ordinal.add_one_eq_succ` `Nat.cast_succ` `Ordinal.nat_lt_omega0` `Ordinal.opow_le_opow_right` `Ordinal.one_le_iff_ne_zero` `pos_iff_ne_zero` `le_add_self` `Ordinal.principal_add_omega0_opow` `Ordinal.opow_succ` `mul_assoc` `mul_lt_mul_of_pos_left` `Ordinal.instPosMulStrictMono` `Ordinal.opow_add` `NFBelow.repr_lt` `NF.below_of_lt` `Ordinal.instAddLeftStrictMono` `Ordinal.instAddLeftReflectLT` `add_lt_add_iff_left` `Ordinal.mul_lt_omega0_opow` `mul_le_mul_right` `Ordinal.mulLeftMono` `Order.succ_le_succ_iff` `Ordinal.instNoMaxOrder` `Nat.cast_le` `Ordinal.instAddLeftMono` `Ordinal.instZeroLEOneClass` `Ordinal.instCharZero` `le_of_lt` `Ordinal.natCast_succ` `dvd_add` `Ordinal.leftDistribClass` `dvd_mul_of_dvd_left` `Ordinal.opow_dvd_opow` `mul_add` `add_assoc` `Ordinal.add_mul_of_isSuccLimit` `Ordinal.add_absorp` `NF.snd'` `Order.one_le_iff_pos` `Ordinal.instNeZeroOne` `Nat.cast_pos'` `PNat.pos` `Ordinal.isSuccLimit_iff_omega0_dvd` `ne_of_gt` `Ordinal.mul_omega0_dvd` `Ordinal.opow_natCast` `Ordinal.add_mul_succ` `omega0_le_oadd`
`repr_scale` 📖	mathematical	—	`repr` `scale` `Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Ordinal.monoidWithZero` `Ordinal.instPow` `Ordinal.omega0`	—	`scale_eq_mul` `repr_mul` `NF.oadd_zero` `Nat.cast_one` `mul_one` `add_zero`
`repr_sub` 📖	mathematical	—	`repr` `ONote` `instSub` `Ordinal` `Ordinal.sub`	—	`Ordinal.zero_sub` `Ordinal.sub_zero` `NF.snd` `cmp_compares` `NF.fst` `Ordinal.sub_eq_zero_iff_le` `le_of_lt` `oadd_lt_oadd_1` `Ordinal.add_sub_add_cancel` `oadd_lt_oadd_2` `lt_of_le_of_ne` `tsub_eq_zero_iff_le` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `PNat.eq` `Nat.cast_add` `Nat.cast_one` `tsub_eq_iff_eq_add_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `add_comm` `mul_add` `Ordinal.leftDistribClass` `add_assoc` `Ordinal.sub_eq_of_add_eq` `Ordinal.add_absorp` `NFBelow.repr_lt` `NF.snd'` `le_trans` `Ordinal.le_mul_left` `Nat.cast_lt` `Ordinal.instAddLeftMono` `Ordinal.instZeroLEOneClass` `Ordinal.instCharZero` `le_self_add` `Ordinal.canonicallyOrderedAdd` `NF.below_of_lt` `omega0_le_oadd`
`repr_zero` 📖	mathematical	—	`repr` `ONote` `instZero` `Ordinal` `Ordinal.zero`	—	—
`scale_eq_mul` 📖	mathematical	—	`scale` `ONote` `instMul` `oadd` `PNat` `instOfNatPNatOfNeZeroNat` `instZero`	—	`NF.snd` `add_nf` `NF.zero` `repr_add` `add_zero` `NF.zero_of_zero` `MulZeroClass.mul_zero` `one_mul`
`scale_opowAux` 📖	mathematical	—	`repr` `opowAux` `Ordinal` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Ordinal.monoidWithZero` `Ordinal.instPow` `Ordinal.omega0` `ONote` `instZero`	—	`MulZeroClass.mul_zero` `Nat.cast_add` `Nat.cast_one` `add_zero` `Ordinal.opow_zero` `one_mul` `opowAux.eq_1` `opowAux.eq_3` `mulNat_eq_mul` `repr_add` `nf_scale` `add_nf` `mul_nf` `nf_ofNat` `nf_opowAux` `repr_scale` `repr_mul` `repr_ofNat` `Ordinal.opow_add` `mul_assoc` `NF.zero` `mul_add` `Ordinal.leftDistribClass`
`split_add_lt` 📖	mathematical	`split` `ONote` `oadd`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.add` `repr` `AddMonoidWithOne.toNatCast` `Ordinal.addMonoidWithOne` `Ordinal.instPow` `Ordinal.omega0`	—	`nf_repr_split` `NF.of_dvd_omega0` `split_dvd` `Ordinal.principal_add_omega0_opow` `NFBelow.repr_lt` `NF.snd'` `lt_of_lt_of_le` `Ordinal.nat_lt_omega0` `Ordinal.opow_one` `Ordinal.opow_le_opow_right` `Ordinal.omega0_pos` `Ordinal.one_le_iff_ne_zero`
`split_dvd` 📖	mathematical	`split` `ONote`	`Ordinal` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `Ordinal.monoidWithZero` `Ordinal.omega0` `repr`	—	`split_eq_scale_split'` `nf_repr_split'` `repr_scale` `nf_one` `repr_one` `Nat.cast_one` `Ordinal.opow_one`
`split_eq_scale_split'` 📖	mathematical	`split'` `ONote`	`split` `scale` `instOne`	—	`NF.snd` `add_nf` `nf_one` `sub_nf` `NF.fst` `repr_add` `repr_one` `Nat.cast_one` `repr_sub` `NF.zero` `Ordinal.add_sub_cancel_of_le` `Ordinal.one_le_iff_ne_zero`
`sub_nf` 📖	mathematical	—	`NF` `ONote` `instSub`	—	`sub_nfBelow`
`sub_nfBelow` 📖	mathematical	`NFBelow`	`ONote` `instSub`	—	`NFBelow.snd` `NF.snd` `cmp_compares` `NFBelow.fst` `NF.fst` `NFBelow.mono` `le_of_lt` `NFBelow.lt` `NFBelow.oadd`
`zero_add` 📖	mathematical	—	`ONote` `instAdd` `instZero`	—	—
`zero_def` 📖	mathematical	—	`zero` `ONote` `instZero`	—	—
`zero_lt_one` 📖	mathematical	—	`ONote` `Preorder.toLT` `instPreorder` `instZero` `instOne`	—	`repr_one` `Nat.cast_one` `Ordinal.instZeroLEOneClass` `Ordinal.instNeZeroOne`

ONote.NF

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`below_of_lt` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `ONote.repr`	`ONote.NFBelow` `ONote.oadd`	—	—
`below_of_lt'` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `ONote.repr` `Ordinal.instPow` `Ordinal.omega0`	`ONote.NFBelow`	—	`below_of_lt` `Ordinal.opow_lt_opow_iff_right` `Ordinal.one_lt_omega0` `lt_of_le_of_lt` `ONote.omega0_le_oadd`
`fst` 📖	mathematical	—	`ONote.NF`	—	`ONote.NFBelow.fst`
`oadd` 📖	mathematical	`ONote.NFBelow` `ONote.repr`	`ONote.NF` `ONote.oadd`	—	`ONote.NFBelow.oadd` `Order.lt_succ` `Ordinal.instNoMaxOrder`
`oadd_zero` 📖	mathematical	—	`ONote.NF` `ONote.oadd` `ONote` `ONote.instZero`	—	`oadd`
`of_dvd_omega0` 📖	—	`Ordinal` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `Ordinal.monoidWithZero` `Ordinal.omega0` `ONote.repr` `ONote.oadd`	—	—	`Ordinal.opow_one` `Ordinal.one_le_iff_ne_zero` `of_dvd_omega0_opow`
`of_dvd_omega0_opow` 📖	mathematical	`Ordinal` `semigroupDvd` `SemigroupWithZero.toSemigroup` `MonoidWithZero.toSemigroupWithZero` `Ordinal.monoidWithZero` `Ordinal.instPow` `Ordinal.omega0` `ONote.repr` `ONote.oadd`	`Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder`	—	`zero` `le_of_not_gt` `not_le_of_gt` `ONote.NFBelow.repr_lt` `below_of_lt` `Ordinal.le_of_dvd` `Ordinal.dvd_add_iff` `Dvd.dvd.mul_right` `Ordinal.opow_dvd_opow`
`out` 📖	mathematical	—	`ONote.NFBelow`	—	—
`snd` 📖	mathematical	—	`ONote.NF`	—	`snd'`
`snd'` 📖	mathematical	—	`ONote.NFBelow` `ONote.repr`	—	`ONote.NFBelow.snd`
`zero` 📖	mathematical	—	`ONote.NF` `ONote` `ONote.instZero`	—	—
`zero_of_zero` 📖	—	`ONote` `ONote.instZero`	—	—	`snd'`

ONote.NFBelow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fst` 📖	mathematical	`ONote.NFBelow` `ONote.oadd`	`ONote.NF`	—	—
`lt` 📖	mathematical	`ONote.NFBelow` `ONote.oadd`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `ONote.repr`	—	—
`mono` 📖	—	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `ONote.NFBelow`	—	—	`lt_of_lt_of_le`
`oadd` 📖	mathematical	`ONote.NFBelow` `ONote.repr` `Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder`	`ONote.oadd`	—	—
`repr_lt` 📖	mathematical	`ONote.NFBelow`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `ONote.repr` `Ordinal.instPow` `Ordinal.omega0`	—	`Ordinal.opow_pos` `Ordinal.omega0_pos` `ONote.repr.eq_2` `LT.lt.trans_le` `add_lt_add_right` `Ordinal.instAddLeftStrictMono` `Ordinal.mul_succ` `le_imp_le_of_le_of_le` `mul_le_mul_right` `Ordinal.mulLeftMono` `Order.succ_le_of_lt` `Ordinal.nat_lt_omega0` `le_refl` `Ordinal.opow_succ` `Ordinal.opow_le_opow`
`snd` 📖	mathematical	`ONote.NFBelow` `ONote.oadd`	`ONote.repr`	—	—

(root)

Definitions

Name	Category	Theorems
`NONote` 📖	CompOp	6 math math: `NONote.repr_add`, `NONote.cmp_compares`, `NONote.lt_wf`, `NONote.repr_sub`, `NONote.repr_mul`, `NONote.instWellFoundedLT`
`ONote` 📖	CompData	43 math math: `ONote.repr_one`, `ONote.ofNat_succ`, `ONote.NFBelow_zero`, `ONote.zero_add`, `ONote.add_nfBelow`, `ONote.cmp_compares`, `ONote.repr_mul`, `ONote.ofNat_one`, `ONote.oadd_add`, `ONote.lt_def`, `ONote.oadd_mul_nfBelow`, `ONote.repr_add`, `ONote.repr_zero`, `ONote.nf_opow`, `ONote.fundamentalSequenceProp_inl_none`, `ONote.zero_lt_one`, `ONote.NF.oadd_zero`, `ONote.ofNat_zero`, `ONote.le_def`, `ONote.mulNat_eq_mul`, `ONote.repr_opow`, `ONote.sub_nf`, `ONote.fundamentalSequenceProp_inl_some`, `ONote.nf_one`, `ONote.sub_nfBelow`, `ONote.mul_nf`, `ONote.fundamentalSequenceProp_inr`, `ONote.opow_def`, `ONote.repr_opow_aux₂`, `ONote.oadd_lt_oadd_2`, `ONote.scale_eq_mul`, `ONote.fastGrowing_one`, `ONote.fastGrowing_zero`, `ONote.scale_opowAux`, `ONote.fastGrowing_def`, `ONote.oadd_pos`, `ONote.zero_def`, `ONote.oadd_mul`, `ONote.fastGrowing_two`, `ONote.repr_sub`, `NONote.NF`, `ONote.add_nf`, `ONote.NF.zero`
`instDecidableEqNONote` 📖	CompOp	—
`instDecidableEqONote` 📖	CompOp	1 math math: `ONote.oadd_mul`

instDecidableEqONote

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

---

← Back to Index