Group

📁 Source: Mathlib/Order/CompleteLattice/Group.lean

Statistics

Metric	Count
Definitions	0
Theorems iSup_add_le, iSup_mul_le, iSup₂_add_le, iSup₂_mul_le, le_iInf_add, le_iInf_mul, le_iInf₂_add, le_iInf₂_mul	8
Total	8

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iSup_add_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf iSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup	—	iSup_le add_le_add le_iSup
iSup_mul_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf iSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup	—	iSup_le mul_le_mul' le_iSup
iSup₂_add_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf iSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup	—	le_trans iSup_mono iSup_add_le
iSup₂_mul_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf iSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup	—	le_trans iSup_mono iSup_mul_le
le_iInf_add 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf iInf CompleteSemilatticeInf.toInfSet	—	iSup_add_le OrderDual.addLeftMono OrderDual.addRightMono
le_iInf_mul 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf iInf CompleteSemilatticeInf.toInfSet	—	iSup_mul_le OrderDual.mulLeftMono OrderDual.mulRightMono
le_iInf₂_add 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf iInf CompleteSemilatticeInf.toInfSet	—	iSup₂_add_le OrderDual.addLeftMono OrderDual.addRightMono
le_iInf₂_mul 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf iInf CompleteSemilatticeInf.toInfSet	—	iSup₂_mul_le OrderDual.mulLeftMono OrderDual.mulRightMono

---

← Back to Index