Structures · Order
OrderBot
An order is an OrderBot if it has a least element.
We state this using a data mixin, holding the value of ⊥ and the least element constraint.
- Defined in
- Mathlib.Order.BoundedOrder.Basic
- Shape
- One type argument · adds bot_le
Extends1
Extended by7
Concrete types that are instances73
- Nat
- NNReal
- ENNReal
- Filter.Germ
- NNRat
- ENat
- MeasureTheory.SimpleFunc
- Finsupp
- Interval
- DFinsupp
- SetSemiring
- PNat
- Ordinal
- FractionalIdeal
- Cardinal
- AlgebraicGeometry.Scheme.IdealSheafData
- Associates
- PrimeSpectrum
- Ordinal.ToType
- TopologicalSpace.Compacts
- ProbabilityTheory.Kernel
- ValuativeRel.ValueGroupWithZero
- MeasureTheory.OuterMeasure
- Part
- PrimeMultiset
- Seminorm
- Finpartition
- LinearPMap
- MonomialOrder.syn
- ClosedSubmodule
- SimpleGraph.Finsubgraph
- DegLex
- CategoryTheory.Subobject
- Nucleus
- OrderType
- Order.Ideal
- TopologicalSpace.CompactOpens
- StructureGroupoid
- CategoryTheory.Pretopology
- FiniteGaloisIntermediateField
- YoungDiagram
- Graph
- DiscreteQuotient
- BotHom
- InfHom
- SupHom
- Order.PFilter
- BoxIntegral.Prepartition
- SupBotHom
- PEquiv
- Geometry.SimplicialComplex
- sSupHom
- PseudoMetric
- RootedTree.α
- IntermediateField.Lifts
- SemilatSupCat.X
- Subtype
- Prod
- OrderDual
- Set.Elem
- ULift
- Lex
- Shrink
- WithTop
- WithBot
- Colex
- Multiplicative
- Additive
- Submodule
- WithZero
- Multiset
- Finset
- OrderHom
How is a type an instance?
Loading the hierarchy index…
Assumed by1,194
- Disjoint
- Finset.sup
- bot_le
- Set.PairwiseDisjoint
- Finpartition.parts
- eq_bot_iff
- IsAtom
- Disjoint.symm
- le_bot_iff
- Ne.bot_lt
- Finset.le_sup
- bot_eq_zero'
- disjoint_iff
- Finset.sup_empty
- Disjoint.mono
- disjoint_iff_inf_le
- Disjoint.mono_right
- GaloisConnection.l_bot
- Filter.isCobounded_le_of_bot
- bot_lt_iff_ne_bot
- bot_unique
- Filter.isBounded_ge_of_bot
- Finset.SupIndep
- Disjoint.eq_bot
- Disjoint.le_bot
- Disjoint.mono_left
- AddMonoidAlgebra.supDegree
- disjoint_comm
- CategoryTheory.TransfiniteCompositionOfShape.F
- Finset.sup_le
- MeasureTheory.upperCrossingTime
- Finset.sup_singleton
- Finset.sup'_eq_sup
- Finset.sup_insert
- bot_sup_eq
- sup_bot_eq
- OrderBot.bddBelow
- bot_eq_zero
- Finset.sup_cons
- OrderIso.map_bot
- WithBot.succ
- disjoint_self
- Finset.sup_image
- LT.lt.ne_bot
- Finset.sup_mono
- CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape
- Finset.sup_le_iff
- CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape
- AddMonoidAlgebra.leadingCoeff
- CategoryTheory.SmallObject.SuccStruct.Iteration.F