Documentation Verification Report

LocallyFiniteOrder

📁 Source: Mathlib/Algebra/Order/Monoid/LocallyFiniteOrder.lean

Statistics

Metric	Count
Definitions `LocallyFiniteOrder`, `addMonoidHom`, `orderAddMonoidEquiv`, `orderAddMonoidHom`, `orderMonoidEquiv`, `orderMonoidHom`, `orderMonoidWithZeroEquiv`, `orderMonoidWithZeroHom`	8
Theorems `card_Ico_add_right`, `card_Ico_mul_right`, `orderAddMonoidEquiv_apply`, `orderAddMonoidHom_apply`, `orderAddMonoidHom_bijective`, `orderAddMonoidHom_strictMono`, `orderAddMonoidHom_toAddMonoidHom`, `orderMonoidHom_strictMono`, `orderMonoidWithZeroHom_strictMono`, `card_Ico_one_mul`, `card_Ico_zero_add`	11
Total	19

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_Ico_add_right` 📖	mathematical	—	`card` `Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `ext` `mem_Ico` `mem_map` `ExistsAddOfLE.exists_add_of_le` `le_add_iff_nonneg_right` `IsOrderedAddMonoid.toAddLeftMono` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `add_right_comm` `add_lt_add_iff_right` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `covariant_swap_add_of_covariant_add` `contravariant_swap_add_of_contravariant_add` `add_assoc` `add_comm` `add_le_add_iff_right` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `card_map`
`card_Ico_mul_right` 📖	mathematical	—	`card` `Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `CancelCommMonoid.toCommMonoid`	—	`RightCancelSemigroup.toIsRightCancelMul` `ext` `ExistsMulOfLE.exists_mul_of_le` `IsOrderedMonoid.toMulLeftMono` `IsLeftCancelMul.mulLeftReflectLE_of_mulLeftReflectLT` `LeftCancelSemigroup.toIsLeftCancelMul` `contravariant_lt_of_covariant_le` `mul_right_comm` `IsRightCancelMul.mulRightStrictMono_of_mulRightMono` `covariant_swap_mul_of_covariant_mul` `contravariant_swap_mul_of_contravariant_mul` `mul_assoc` `mul_comm` `IsRightCancelMul.mulRightReflectLE_of_mulRightReflectLT` `card_map`

LocallyFiniteOrder

Definitions

Name	Category	Theorems
`addMonoidHom` 📖	CompOp	3 math math: `orderAddMonoidHom_apply`, `orderAddMonoidHom_toAddMonoidHom`, `orderAddMonoidEquiv_apply`
`orderAddMonoidEquiv` 📖	CompOp	1 math math: `orderAddMonoidEquiv_apply`
`orderAddMonoidHom` 📖	CompOp	4 math math: `orderAddMonoidHom_bijective`, `orderAddMonoidHom_strictMono`, `orderAddMonoidHom_apply`, `orderAddMonoidHom_toAddMonoidHom`
`orderMonoidEquiv` 📖	CompOp	—
`orderMonoidHom` 📖	CompOp	1 math math: `orderMonoidHom_strictMono`
`orderMonoidWithZeroEquiv` 📖	CompOp	—
`orderMonoidWithZeroHom` 📖	CompOp	1 math math: `orderMonoidWithZeroHom_strictMono`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`orderAddMonoidEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidIso` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLatticeInt` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `OrderAddMonoidIso.instEquivLike` `orderAddMonoidEquiv` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Int.instAddMonoid` `AddMonoidHom.instFunLike` `addMonoidHom`	—	—
`orderAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidHom` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLatticeInt` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Int.instAddMonoid` `OrderAddMonoidHom.instFunLike` `orderAddMonoidHom` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoidHom.instFunLike` `addMonoidHom`	—	—
`orderAddMonoidHom_bijective` 📖	mathematical	—	`Function.Bijective` `DFunLike.coe` `OrderAddMonoidHom` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLatticeInt` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Int.instAddMonoid` `OrderAddMonoidHom.instFunLike` `orderAddMonoidHom`	—	`StrictMono.injective` `orderAddMonoidHom_strictMono` `exists_zero_lt` `LT.lt.le` `exists_covBy_of_wellFoundedLT` `IsWellOrder.toIsWellFounded` `isWellOrder_lt` `Finite.to_wellFoundedLT` `Finite.of_fintype` `LT.lt.not_ge` `Finset.ext` `LE.le.trans` `lt_of_le_of_ne` `Finset.card_singleton` `Nat.cast_one` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `map_zsmul` `AddMonoidHom.instAddMonoidHomClass` `mul_one`
`orderAddMonoidHom_strictMono` 📖	mathematical	—	`StrictMono` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLatticeInt` `DFunLike.coe` `OrderAddMonoidHom` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Int.instAddMonoid` `OrderAddMonoidHom.instFunLike` `orderAddMonoidHom`	—	`strictMono_iff_map_pos` `Int.instIsOrderedAddMonoid` `OrderAddMonoidHom.instAddMonoidHomClass` `Finset.Ico_eq_empty_of_le` `IsOrderedAddMonoid.toAddLeftMono` `LT.lt.le` `Nat.cast_zero` `sub_zero`
`orderAddMonoidHom_toAddMonoidHom` 📖	mathematical	—	`AddMonoidHomClass.toAddMonoidHom` `OrderAddMonoidHom` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLatticeInt` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Int.instAddMonoid` `AddZeroClass.toAddZero` `OrderAddMonoidHom.instFunLike` `OrderAddMonoidHom.instAddMonoidHomClass` `orderAddMonoidHom` `addMonoidHom`	—	`OrderAddMonoidHom.instAddMonoidHomClass`
`orderMonoidHom_strictMono` 📖	mathematical	—	`StrictMono` `Multiplicative` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Multiplicative.preorder` `instLatticeInt` `DFunLike.coe` `OrderMonoidHom` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `OrderMonoidHom.instFunLike` `orderMonoidHom`	—	`orderAddMonoidHom_strictMono` `Additive.isOrderedAddMonoid`
`orderMonoidWithZeroHom_strictMono` 📖	mathematical	—	`StrictMono` `WithZero` `Multiplicative` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `WithZero.instPreorder` `Multiplicative.preorder` `instLatticeInt` `DFunLike.coe` `OrderMonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `WithZero.instMulZeroOneClass` `Multiplicative.mulOneClass` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `OrderMonoidWithZeroHom.instFunLike` `orderMonoidWithZeroHom`	—	`Units.isOrderedMonoid` `LinearOrderedCommMonoidWithZero.toIsOrderedMonoid` `orderMonoidHom_strictMono` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass`

(root)

Definitions

Name	Category	Theorems
`LocallyFiniteOrder` 📖	CompData	2 math math: `instSubsingletonLocallyFiniteOrder`, `Valued.integer.locallyFiniteOrder_units_mrange_of_isCompact_integer`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_Ico_one_mul` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `CancelCommMonoid.toCommMonoid`	`Finset.card` `Finset.Ico` `MulOne.toMul`	—	`one_mul` `Finset.Ico_union_Ico` `inf_of_le_left` `sup_of_le_right` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `IsRightCancelMul.mulRightReflectLE_of_mulRightReflectLT` `RightCancelSemigroup.toIsRightCancelMul` `contravariant_swap_mul_of_contravariant_mul` `contravariant_lt_of_covariant_le` `Right.one_le_mul` `Finset.card_union` `Finset.card_Ico_mul_right` `add_comm` `Finset.Ico_inter_Ico_consecutive` `tsub_zero` `Nat.instOrderedSub`
`card_Ico_zero_add` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid`	`Finset.card` `Finset.Ico` `AddZero.toAdd`	—	`zero_add` `Finset.Ico_union_Ico` `inf_of_le_left` `sup_of_le_right` `le_add_iff_nonneg_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Right.add_nonneg` `le_refl` `Finset.card_union` `Finset.card_Ico_add_right` `add_comm` `Finset.Ico_inter_Ico_consecutive` `tsub_zero` `Nat.instOrderedSub`

---

← Back to Index