WithTop

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

Statistics

Metric	Count
Definitions	0
Theorems isOrderedAddMonoid, le_add_self, le_self_add, canonicallyOrderedAdd, isOrderedAddMonoid	5
Total	5

WithBot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOrderedAddMonoid 📖	mathematical	—	IsOrderedAddMonoid WithBot addCommMonoid instPartialOrder	—	add_le_add_left addRightMono covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono
le_add_self 📖	mathematical	—	WithBot instLE add AddCommMagma.toAdd	—	add_bot coe_add coe_le_coe le_add_self
le_self_add 📖	mathematical	—	WithBot instLE add	—	coe_add coe_le_coe le_self_add

WithTop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
canonicallyOrderedAdd 📖	mathematical	—	CanonicallyOrderedAdd WithTop add Preorder.toLE instPreorder	—	existsAddOfLE CanonicallyOrderedAdd.toExistsAddOfLE le_rfl le_top coe_le_coe le_add_self le_self_add
isOrderedAddMonoid 📖	mathematical	—	IsOrderedAddMonoid WithTop addCommMonoid instPartialOrder	—	add_le_add_left addRightMono covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono

---

← Back to Index