CantorNormalForm

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

Statistics

Metric	Count
Definitions `CNF`, `coeff`, `rec`, `CNFRec`	4
Theorems `coeff_of_le_one`, `coeff_of_mem_CNF`, `coeff_of_not_mem_CNF`, `coeff_one_left`, `coeff_zero_apply`, `coeff_zero_left`, `coeff_zero_right`, `foldr`, `fst_le_log`, `lt_snd`, `ne_zero`, `of_le_one`, `of_lt`, `one_left`, `rec_pos`, `rec_zero`, `snd_lt`, `sorted`, `zero_left`, `zero_right`, `CNFRec_pos`, `CNFRec_zero`, `CNF_foldr`, `CNF_fst_le_log`, `CNF_lt_snd`, `CNF_ne_zero`, `CNF_of_le_one`, `CNF_of_lt`, `CNF_snd_lt`, `CNF_sorted`, `CNF_zero`, `one_CNF`, `zero_CNF`	33
Total	37

Ordinal

Definitions

Name	Category	Theorems
`CNF` 📖	CompOp	16 math math: `CNF_foldr`, `CNF.zero_left`, `CNF.sorted`, `CNF_ne_zero`, `zero_CNF`, `CNF.of_lt`, `CNF_sorted`, `CNF.of_le_one`, `CNF.foldr`, `CNF.one_left`, `CNF_of_le_one`, `CNF.ne_zero`, `CNF_of_lt`, `one_CNF`, `CNF_zero`, `CNF.zero_right`
`CNFRec` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`CNFRec_pos` 📖	mathematical	—	`Ordinal` `mod` `instPow` `log`	—	`CNF.rec_pos`
`CNFRec_zero` 📖	mathematical	—	`Ordinal` `zero`	—	`CNF.rec_zero`
`CNF_foldr` 📖	mathematical	—	`Ordinal` `add` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `monoidWithZero` `instPow` `zero` `CNF`	—	`CNF.foldr`
`CNF_fst_le_log` 📖	mathematical	`Ordinal` `CNF`	`Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `log`	—	`CNF.fst_le_log`
`CNF_lt_snd` 📖	mathematical	`Ordinal` `CNF`	`Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `zero`	—	`CNF.lt_snd`
`CNF_ne_zero` 📖	mathematical	—	`CNF` `Ordinal` `log` `div` `instPow` `mod`	—	`CNF.ne_zero`
`CNF_of_le_one` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `one`	`CNF` `zero`	—	`CNF.of_le_one`
`CNF_of_lt` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder`	`CNF` `zero`	—	`CNF.of_lt`
`CNF_snd_lt` 📖	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `one` `CNF`	—	—	`CNF.snd_lt`
`CNF_sorted` 📖	mathematical	—	`List.SortedGT` `Ordinal` `PartialOrder.toPreorder` `partialOrder` `CNF`	—	`CNF.sorted`
`CNF_zero` 📖	mathematical	—	`CNF` `Ordinal` `zero`	—	`CNF.zero_right`
`one_CNF` 📖	mathematical	—	`CNF` `Ordinal` `one` `zero`	—	`CNF.one_left`
`zero_CNF` 📖	mathematical	—	`CNF` `Ordinal` `zero`	—	`CNF.zero_left`

Ordinal.CNF

Definitions

Name	Category	Theorems
`coeff` 📖	CompOp	7 math math: `coeff_zero_left`, `coeff_zero_apply`, `coeff_of_not_mem_CNF`, `coeff_of_mem_CNF`, `coeff_one_left`, `coeff_zero_right`, `coeff_of_le_one`
`rec` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_of_le_one` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.one`	`coeff` `Finsupp.single` `Ordinal.zero`	—	`Finsupp.ext` `eq_or_ne` `coeff_zero_right` `Finsupp.single_zero` `coeff_of_mem_CNF` `of_le_one` `Finsupp.single_eq_same` `Finsupp.single_eq_of_ne` `coeff_of_not_mem_CNF`
`coeff_of_mem_CNF` 📖	mathematical	`Ordinal` `Ordinal.CNF`	`DFunLike.coe` `Finsupp` `Ordinal.zero` `Finsupp.instFunLike` `coeff`	—	`coeff.eq_1` `AList.lookupFinsupp_apply` `AList.mem_lookup_iff`
`coeff_of_not_mem_CNF` 📖	mathematical	`Ordinal` `Ordinal.CNF`	`DFunLike.coe` `Finsupp` `Ordinal.zero` `Finsupp.instFunLike` `coeff`	—	`coeff.eq_1` `AList.lookupFinsupp_apply` `AList.lookup_eq_none`
`coeff_one_left` 📖	mathematical	—	`coeff` `Ordinal` `Ordinal.one` `Finsupp.single` `Ordinal.zero`	—	`coeff_of_le_one` `le_rfl`
`coeff_zero_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `Ordinal` `Ordinal.zero` `Finsupp.instFunLike` `coeff`	—	`coeff_of_not_mem_CNF` `zero_right`
`coeff_zero_left` 📖	mathematical	—	`coeff` `Ordinal` `Ordinal.zero` `Finsupp.single`	—	`coeff_of_le_one` `zero_le_one` `Ordinal.instZeroLEOneClass`
`coeff_zero_right` 📖	mathematical	—	`coeff` `Ordinal` `Ordinal.zero` `Finsupp` `Finsupp.instZero`	—	`Finsupp.ext` `coeff_zero_apply`
`foldr` 📖	mathematical	—	`Ordinal` `Ordinal.add` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Ordinal.monoidWithZero` `Ordinal.instPow` `Ordinal.zero` `Ordinal.CNF`	—	`zero_right` `ne_zero` `Ordinal.div_add_mod`
`fst_le_log` 📖	mathematical	`Ordinal` `Ordinal.CNF`	`Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.log`	—	`zero_right` `Ordinal.log_zero_right` `Ordinal.canonicallyOrderedAdd` `instIsEmptyFalse` `ne_zero` `le_refl` `LE.le.trans` `Ordinal.log_mono_right` `LT.lt.le` `Ordinal.mod_opow_log_lt_self`
`lt_snd` 📖	mathematical	`Ordinal` `Ordinal.CNF`	`Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.zero`	—	`zero_right` `instIsEmptyFalse` `ne_zero` `Ordinal.div_opow_log_pos`
`ne_zero` 📖	mathematical	—	`Ordinal.CNF` `Ordinal` `Ordinal.log` `Ordinal.div` `Ordinal.instPow` `Ordinal.mod`	—	`rec_pos`
`of_le_one` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.one`	`Ordinal.CNF` `Ordinal.zero`	—	`Ordinal.le_one_iff` `zero_left` `one_left`
`of_lt` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder`	`Ordinal.CNF` `Ordinal.zero`	—	`ne_zero` `Ordinal.log_eq_zero` `Ordinal.opow_zero` `Ordinal.div_one` `Ordinal.mod_one` `zero_right`
`one_left` 📖	mathematical	—	`Ordinal.CNF` `Ordinal` `Ordinal.one` `Ordinal.zero`	—	`ne_zero` `Ordinal.log_one_left` `Ordinal.opow_zero` `Ordinal.div_one` `Ordinal.mod_one` `zero_right`
`rec_pos` 📖	mathematical	—	`Ordinal` `Ordinal.mod` `Ordinal.instPow` `Ordinal.log`	—	—
`rec_zero` 📖	mathematical	—	`Ordinal` `Ordinal.zero`	—	—
`snd_lt` 📖	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.one` `Ordinal.CNF`	—	—	`zero_right` `instIsEmptyFalse` `ne_zero` `Ordinal.div_opow_log_lt`
`sorted` 📖	mathematical	—	`List.SortedGT` `Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.CNF`	—	`zero_right` `le_or_gt` `of_le_one` `lt_or_ge` `of_lt` `ne_zero` `LE.le.trans_lt` `fst_le_log` `Ordinal.log_mod_opow_log_lt_log_self`
`zero_left` 📖	mathematical	—	`Ordinal.CNF` `Ordinal` `Ordinal.zero`	—	`ne_zero` `Ordinal.log_zero_left` `Ordinal.opow_zero` `Ordinal.div_one` `Ordinal.mod_one` `zero_right`
`zero_right` 📖	mathematical	—	`Ordinal.CNF` `Ordinal` `Ordinal.zero`	—	`rec_zero`

---

← Back to Index