Lattice

📁 Source: Mathlib/Algebra/Order/Group/Lattice.lean

Statistics

Metric	Count
Definitions `toDistribLattice`, `toDistribLattice`	2
Theorems `add_inf`, `add_sup`, `div_inf`, `div_sup`, `inf_add`, `inf_add_sup`, `inf_div`, `inf_mul`, `inf_mul_sup`, `inf_sub`, `inv_inf`, `inv_sup`, `mul_inf`, `mul_sup`, `neg_inf`, `neg_sup`, `nsmul_two_semiclosed`, `pow_two_semiclosed`, `sub_inf`, `sub_sup`, `sup_add`, `sup_div`, `sup_mul`, `sup_sub`	24
Total	26

AddCommGroup

Definitions

Name	Category	Theorems
`toDistribLattice` 📖	CompOp	—

CommGroup

Definitions

Name	Category	Theorems
`toDistribLattice` 📖	CompOp	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_inf` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`OrderIso.map_inf`
`add_sup` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`OrderIso.map_sup`
`div_inf` 📖	mathematical	—	`DivInvMonoid.toDiv` `Group.toDivInvMonoid` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`OrderIso.map_inf`
`div_sup` 📖	mathematical	—	`DivInvMonoid.toDiv` `Group.toDivInvMonoid` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`OrderIso.map_sup`
`inf_add` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`OrderIso.map_inf`
`inf_add_sup` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`add_sup` `add_neg_cancel_right` `add_neg_cancel_comm` `neg_inf` `covariant_swap_add_of_covariant_add` `sup_comm` `add_comm` `neg_add_cancel_right`
`inf_div` 📖	mathematical	—	`DivInvMonoid.toDiv` `Group.toDivInvMonoid` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`OrderIso.map_inf`
`inf_mul` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`OrderIso.map_inf`
`inf_mul_sup` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`mul_sup` `mul_inv_cancel_right` `mul_inv_cancel_comm` `inv_inf` `covariant_swap_mul_of_covariant_mul` `sup_comm` `mul_comm` `inv_mul_cancel_right`
`inf_sub` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`OrderIso.map_inf`
`inv_inf` 📖	mathematical	—	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`OrderIso.map_inf`
`inv_sup` 📖	mathematical	—	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`OrderIso.map_sup`
`mul_inf` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`OrderIso.map_inf`
`mul_sup` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`OrderIso.map_sup`
`neg_inf` 📖	mathematical	—	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`OrderIso.map_inf`
`neg_sup` 📖	mathematical	—	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`OrderIso.map_sup`
`nsmul_two_semiclosed` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	—	`add_inf` `inf_add` `two_nsmul` `add_zero` `zero_add` `inf_assoc` `inf_left_idem` `inf_comm` `inf_of_le_left` `inf_eq_right` `add_eq_left` `AddLeftCancelSemigroup.toIsLeftCancelAdd`
`pow_two_semiclosed` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—	`mul_inf` `inf_mul` `pow_two` `mul_one` `one_mul` `inf_assoc` `inf_left_idem` `inf_comm` `inf_of_le_left` `inf_eq_right` `mul_eq_left` `LeftCancelSemigroup.toIsLeftCancelMul`
`sub_inf` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`OrderIso.map_inf`
`sub_sup` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`OrderIso.map_sup`
`sup_add` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`OrderIso.map_sup`
`sup_div` 📖	mathematical	—	`DivInvMonoid.toDiv` `Group.toDivInvMonoid` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`OrderIso.map_sup`
`sup_mul` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`OrderIso.map_sup`
`sup_sub` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`OrderIso.map_sup`

---

← Back to Index