Structures · Order
Order.Ideal.IsMaximal
An ideal is maximal if it is maximal in the collection of proper ideals.
Note that IsCoatom is less general because ideals only have a top element when P is directed
and nonempty.
- Defined in
- Mathlib.Order.Ideal
- Shape
- One type argument · adds maximal_proper
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…