Structures · Order
IsUpperModularLattice
An upper modular lattice, aka semimodular lattice, is a lattice where a ⊔ b covers a and b
if either a or b covers a ⊓ b.
- Defined in
- Mathlib.Order.ModularLattice
- Shape
- One type argument · adds covBy_sup_of_inf_covBy
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- OrderDual
How is a type an instance?
Loading the hierarchy index…
Assumed by8
Ancestors0
No ancestors.