Structures · Order
BoundedOrder
A bounded order describes an order (≤) with a top and bottom element,
denoted ⊤ and ⊥ respectively.
- Defined in
- Mathlib.Order.BoundedOrder.Basic
- Shape
- One type argument
Extends2
Extended by1
Concrete types that are instances45
- Bool
- ENNReal
- Filter.Germ
- MeasureTheory.SimpleFunc
- Lat.carrier
- Interval
- Associates
- PrimeSpectrum
- SignType
- TopologicalSpace.Compacts
- SimpleGraph.Subgraph
- CategoryTheory.Subobject
- Nucleus
- TopologicalSpace.CompactOpens
- LinOrd.carrier
- GroupTopology
- AddGroupTopology
- Concept
- DistLat.carrier
- Heyting.Regular
- Booleanisation
- Complementeds
- PartOrd.carrier
- ClopenUpperSet
- Subrepresentation
- InfHom
- SupHom
- BoxIntegral.IntegrationParams
- AddAction.BlockMem
- MulAction.BlockMem
- Subtype
- Prod
- OrderDual
- Set.Elem
- ULift
- Fin
- Lex
- WithTop
- WithBot
- Colex
- Multiplicative
- Additive
- WithZero
- Set
- Finset
How is a type an instance?
Loading the hierarchy index…
Assumed by352
- IsCompl.symm
- IsCompl.disjoint
- IsCompl.codisjoint
- BoundedLatticeHom.comp
- bot_ne_top
- IsComplemented
- IsCompl.sup_eq_top
- Finset.truncatedInf
- BoundedLatticeHom.id
- subsingleton_iff_bot_eq_top
- top_ne_bot
- BoundedOrderHom.comp
- OrderIso.isSimpleOrder_iff
- Complementeds
- BoundedLatticeHom.dual
- IsCompl.inf_eq_bot
- BddDistLat.of
- BddDistLat.ofHom
- BddOrd.of
- BddOrd.ofHom
- subsingleton_of_bot_eq_top
- FinBddDistLat.ofHom
- isCompl_iff
- BoundedOrderHom.id
- OrderIso.complementedLattice_iff
- FinBddDistLat.of
- BoundedOrderHom.dual
- IsCompl.of_eq
- bot_lt_top
- IsCompl.dual
- disjoint_top
- isCompl_top_bot
- isAtom_top
- BoundedLatticeHom.toLatticeHom
- BddLat.of
- eq_top_of_isCompl_bot
- Finset.truncatedInf_of_mem
- OrderIso.complementedLattice
- BoundedOrderHom.toOrderHom
- Finset.truncatedInf_of_notMem
- IsSimpleOrder.equivBool
- Disjoint.le_of_codisjoint
- isAtom_iff_eq_top
- Set.Icc_bot_top
- Continuous.strictMono_of_inj_boundedOrder
- subsingleton_of_top_eq_bot
- IsCompl.isAtom_iff_isCoatom
- IsSimpleOrder.eq_top_of_lt
- OrderIso.isCompl_iff
- OrderIso.isSimpleOrder