CantorNormalForm

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

Statistics

Metric	Count
Definitions `CNF`, `coeff`, `eval`, `rec`	4
Theorems `coeff_eq_zero_of_lt`, `coeff_eval`, `coeff_inj`, `coeff_injective`, `coeff_of_le_one`, `coeff_of_mem_CNF`, `coeff_of_notMem_CNF`, `coeff_of_not_mem_CNF`, `coeff_one_left`, `coeff_opow_mul_add`, `coeff_zero_apply`, `coeff_zero_left`, `coeff_zero_right`, `eval_add`, `eval_coeff`, `eval_lt`, `eval_single`, `eval_single_add`, `eval_single_add'`, `eval_zero_right`, `foldr`, `fst_le_log`, `lt_snd`, `ne_zero`, `of_le_one`, `of_lt`, `one_left`, `opow_mul_add`, `rec_pos`, `rec_zero`, `snd_lt`, `snd_pos`, `sorted`, `sortedGT`, `support_coeff`, `zero_left`, `zero_right`	37
Total	41

Ordinal

Definitions

Name	Category	Theorems
`CNF` 📖	CompOp	11 math math: `CNF.zero_left`, `CNF.sorted`, `CNF.of_lt`, `CNF.sortedGT`, `CNF.support_coeff`, `CNF.of_le_one`, `CNF.foldr`, `CNF.one_left`, `CNF.ne_zero`, `CNF.opow_mul_add`, `CNF.zero_right`

Ordinal.CNF

Definitions

Name	Category	Theorems
`coeff` 📖	CompOp	15 math math: `coeff_injective`, `coeff_eval`, `coeff_zero_left`, `coeff_opow_mul_add`, `coeff_eq_zero_of_lt`, `coeff_zero_apply`, `coeff_of_not_mem_CNF`, `coeff_of_mem_CNF`, `support_coeff`, `coeff_of_notMem_CNF`, `coeff_one_left`, `coeff_zero_right`, `coeff_inj`, `coeff_of_le_one`, `eval_coeff`
`eval` 📖	CompOp	8 math math: `coeff_eval`, `eval_single_add'`, `eval_single`, `eval_lt`, `eval_add`, `eval_zero_right`, `eval_single_add`, `eval_coeff`
`rec` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_eq_zero_of_lt` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.instPow`	`DFunLike.coe` `Finsupp` `Ordinal` `Ordinal.zero` `Finsupp.instFunLike` `coeff`	—	`coeff_of_notMem_CNF` `eq_or_ne` `Ordinal.opow_zero` `Ordinal.instNoMaxOrder` `Ordinal.canonicallyOrderedAdd` `zero_right` `LE.le.not_gt` `Ordinal.opow_le_of_le_log` `fst_le_log`
`coeff_eval` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.one` `DFunLike.coe` `Finsupp` `Ordinal.zero` `Finsupp.instFunLike`	`coeff` `eval`	—	`Finsupp.induction_on_max` `eval_zero_right` `coeff_zero_right` `LT.lt.trans_eq'` `Finsupp.add_apply` `Finsupp.single_eq_of_ne` `LT.lt.ne` `zero_add` `Finsupp.notMem_support_iff` `LT.lt.pos` `Ordinal.canonicallyOrderedAdd` `eval_single_add'` `coeff_opow_mul_add` `Finsupp.single_eq_same` `LT.lt.false` `add_zero` `eval_lt`
`coeff_inj` 📖	mathematical	—	`coeff`	—	`coeff_injective`
`coeff_injective` 📖	mathematical	—	`Ordinal` `Finsupp` `Ordinal.zero` `coeff`	—	`eval_coeff`
`coeff_of_le_one` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.one`	`coeff` `Finsupp.single` `Ordinal` `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_notMem_CNF`
`coeff_of_mem_CNF` 📖	mathematical	`Ordinal` `Ordinal.CNF`	`DFunLike.coe` `Finsupp` `Ordinal` `Ordinal.zero` `Finsupp.instFunLike` `coeff`	—	`AList.lookupFinsupp_apply` `AList.mem_lookup_iff`
`coeff_of_notMem_CNF` 📖	mathematical	`Ordinal` `Ordinal.CNF`	`DFunLike.coe` `Finsupp` `Ordinal` `Ordinal.zero` `Finsupp.instFunLike` `coeff`	—	`Finsupp.notMem_support_iff` `support_coeff` `List.mem_toFinset`
`coeff_of_not_mem_CNF` 📖	mathematical	`Ordinal` `Ordinal.CNF`	`DFunLike.coe` `Finsupp` `Ordinal` `Ordinal.zero` `Finsupp.instFunLike` `coeff`	—	`coeff_of_notMem_CNF`
`coeff_one_left` 📖	mathematical	—	`coeff` `Ordinal` `Ordinal.one` `Finsupp.single` `Ordinal.zero`	—	`coeff_of_le_one` `le_rfl`
`coeff_opow_mul_add` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.one` `Ordinal.instPow`	`coeff` `Ordinal` `Ordinal.add` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Ordinal.monoidWithZero` `Ordinal.instPow` `Finsupp` `Ordinal.zero` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `Ordinal.addMonoidWithOne` `Finsupp.single`	—	`Finsupp.ext` `Finsupp.add_apply` `eq_or_ne` `Finsupp.single_eq_same` `coeff_eq_zero_of_lt` `add_zero` `coeff_of_mem_CNF` `opow_mul_add` `Finsupp.single_eq_of_ne'` `zero_add` `coeff_of_notMem_CNF`
`coeff_zero_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `Ordinal` `Ordinal.zero` `Finsupp.instFunLike` `coeff`	—	`coeff_of_notMem_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`
`eval_add` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder`	`eval` `Finsupp` `Ordinal` `Ordinal.zero` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `Ordinal.addMonoidWithOne` `Ordinal.add`	—	`Finsupp.induction_on_max` `zero_add` `eval_zero_right` `add_assoc` `eval_single_add` `Finset.mem_union` `Finsupp.support_add` `LT.lt.le` `Finsupp.single_eq_same` `eval_single_add'`
`eval_coeff` 📖	mathematical	—	`eval` `coeff`	—	`foldr` `instAntisymmGe` `LE.total'` `support_coeff` `List.toFinset_sort` `List.SortedGT.nodup` `sortedGT` `List.SortedGE.pairwise` `List.SortedGT.sortedGE` `List.foldr_ext` `coeff_of_mem_CNF`
`eval_lt` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `DFunLike.coe` `Finsupp` `Ordinal.zero` `Finsupp.instFunLike`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `eval` `Ordinal.instPow`	—	`Finsupp.induction_on_max` `eval_zero_right` `Ordinal.opow_pos` `LT.lt.false` `eval_single_add'` `Ordinal.opow_mul_add_lt_opow` `LT.lt.trans_eq'` `Finsupp.add_apply` `Finsupp.single_eq_same` `Finsupp.notMem_support_iff` `add_zero` `Finsupp.single_eq_of_ne` `zero_add` `LT.lt.pos` `Ordinal.canonicallyOrderedAdd`
`eval_single` 📖	mathematical	—	`eval` `Finsupp.single` `Ordinal` `Ordinal.zero` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Ordinal.monoidWithZero` `Ordinal.instPow`	—	`instIsEmptyFalse` `add_zero` `eval_zero_right` `eval_single_add'`
`eval_single_add` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder`	`eval` `Finsupp` `Ordinal` `Ordinal.zero` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `Ordinal.addMonoidWithOne` `Finsupp.single` `Ordinal.add` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Ordinal.monoidWithZero` `Ordinal.instPow`	—	`Finsupp.induction_on_max` `add_zero` `eval_single` `eval_zero_right` `LE.le.eq_or_lt` `Finsupp.single_eq_same` `eval_single_add'` `mul_add` `Ordinal.leftDistribClass` `LE.le.lt_of_ne` `LT.lt.not_gt` `Finsupp.single_eq_of_ne` `LT.lt.ne'` `zero_add`
`eval_single_add'` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder`	`eval` `Finsupp` `Ordinal` `Ordinal.zero` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `Ordinal.addMonoidWithOne` `Finsupp.single` `Ordinal.add` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Ordinal.monoidWithZero` `Ordinal.instPow`	—	`eq_or_ne` `Finsupp.single_zero` `zero_add` `MulZeroClass.mul_zero` `Finsupp.notMem_support_iff` `LT.lt.false` `instAntisymmGe` `LE.total'` `Finsupp.support_single_add` `Finset.sort_cons` `LT.lt.le` `Finsupp.single_eq_same` `add_zero` `Ordinal.instIsLeftCancelAdd` `List.foldr_ext` `Finsupp.single_eq_of_ne` `Finset.sort.congr_simp`
`eval_zero_right` 📖	mathematical	—	`eval` `Finsupp` `Ordinal` `Ordinal.zero` `Finsupp.instZero`	—	`instAntisymmGe` `LE.total'` `MulZeroClass.mul_zero` `zero_add` `Finset.sort.congr_simp` `Finset.sort_empty`
`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`	`Ordinal` `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`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.zero`	—	`snd_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` `Ordinal.zero`	—	`Order.le_one_iff` `Ordinal.instNoMaxOrder` `Ordinal.canonicallyOrderedAdd` `zero_left` `one_left`
`of_lt` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder`	`Ordinal.CNF` `Ordinal` `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_of_left_le_one` `instReflLe` `Ordinal.opow_zero` `Ordinal.div_one` `Ordinal.mod_one` `zero_right`
`opow_mul_add` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.one` `Ordinal.instPow`	`Ordinal.CNF` `Ordinal` `Ordinal.add` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Ordinal.monoidWithZero` `Ordinal.instPow`	—	`LT.lt.ne_bot` `ne_zero` `Ordinal.noZeroDivisors` `bot_eq_zero'` `Ordinal.canonicallyOrderedAdd` `Ordinal.log_opow_mul_add` `Ordinal.log_eq_zero` `add_zero` `Ordinal.mul_add_div` `Ordinal.opow_ne_zero` `Ordinal.div_eq_zero_of_lt` `Ordinal.mul_add_mod_self` `Ordinal.mod_eq_of_lt`
`rec_pos` 📖	mathematical	—	`Ordinal` `Ordinal.mod` `Ordinal.instPow` `Ordinal.log`	—	—
`rec_zero` 📖	mathematical	—	`Ordinal` `Ordinal.zero`	—	—
`snd_lt` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.one` `Ordinal.CNF`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder`	—	`zero_right` `instIsEmptyFalse` `ne_zero` `Ordinal.div_opow_log_lt`
`snd_pos` 📖	mathematical	`Ordinal` `Ordinal.CNF`	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.zero`	—	`zero_right` `instIsEmptyFalse` `ne_zero` `Ordinal.div_opow_log_pos`
`sorted` 📖	mathematical	—	`List.SortedGT` `Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.CNF`	—	`sortedGT`
`sortedGT` 📖	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`
`support_coeff` 📖	mathematical	—	`Finsupp.support` `Ordinal` `Ordinal.zero` `coeff` `List.toFinset` `LinearOrder.toDecidableEq` `Ordinal.instLinearOrder` `Ordinal.CNF`	—	`AList.lookupFinsupp_support` `LT.lt.ne'` `snd_pos`
`zero_left` 📖	mathematical	—	`Ordinal.CNF` `Ordinal` `Ordinal.zero`	—	`ne_zero` `Ordinal.log_of_left_le_one` `Ordinal.canonicallyOrderedAdd` `Ordinal.opow_zero` `Ordinal.div_one` `Ordinal.mod_one` `zero_right`
`zero_right` 📖	mathematical	—	`Ordinal.CNF` `Ordinal` `Ordinal.zero`	—	`rec_zero`

---

← Back to Index