Structures · Order
CompleteLinearOrder
A complete linear order is a linear order whose lattice structure is complete.
- Defined in
- Mathlib.Order.CompleteLattice.Defs
- Shape
- One type argument · adds le_himp_iff, himp_bot, sdiff_le_iff, top_sdiff, le_total, toDecidableLE, toDecidableEq, toDecidableLT, compare_eq_compareOfLessAndEq
Extends3
Extended by0
Nothing extends this class yet.
Forgetful instances
Every CompleteLinearOrder is also a
Concrete types that are instances15
- Bool
- ENNReal
- ENat
- EReal
- UpperSet
- LowerSet
- DedekindCut
- OrderDual
- Set.Elem
- Fin
- PUnit
- Lex
- WithTop
- WithBot
- Colex
How is a type an instance?
Loading the hierarchy index…
Assumed by150
- lt_iSup_iff
- sInf_lt_iff
- iSup_eq_top
- iInf_eq_bot
- Pi.Lex.sInf_apply
- iInf₂_eq_bot
- lowerSemicontinuousWithinAt_iSup
- MonotoneOn.map_sSup_of_continuousWithinAt
- Monotone.map_sSup_of_continuousAt
- sSup_ne_of_notMem
- limsup_eq_bot
- lowerSemicontinuousWithinAt_iff_le_liminf
- upperSemicontinuousWithinAt_iInf
- CompleteLinearOrder.toHImp
- iSup_ne_of_notMem
- lowerSemicontinuousAt_iSup
- lowerSemicontinuous_iff_le_liminf
- upperSemicontinuousAt_iInf
- Nat.tendsto_iSup_of_tendsto_limsup
- lowerSemicontinuousOn_iff_le_liminf
- isSaddlePointOn_iff
- Monotone.map_iSup_of_continuousAt
- lowerSemicontinuousAt_iff_le_liminf
- CompleteLinearOrder.toSDiff
- Pi.Lex.sInf_apply_le
- lt_sSup_iff
- sInf_le_iff_forall_lt
- le_sSup_iff_forall_lt
- Pi.Lex.le_sInf_apply
- iInf_lt_iff
- measurable_iSup_of_lowerSemicontinuous
- MeasureTheory.aemeasurable_of_exist_almost_disjoint_supersets
- CompleteLattice.ωScottContinuous.inf
- upperSemicontinuous_iff_limsup_le
- CompleteLinearOrder.toCompl
- tendsto_iSup_of_tendsto_limsup
- Sion.minimax'
- sSup_mem_of_not_isSuccPrelimit
- Pi.Lex.sSup_apply
- upperSemicontinuousWithinAt_iff_limsup_le
- Topology.IsLower.isTopologicalSpace_basis
- Pi.Lex.sSup_apply_le
- upperSemicontinuous_iInf
- Sion.DMCompletion.exists_isSaddlePointOn
- Topology.IsUpper.isTopologicalSpace_basis
- MonotoneOn.map_sInf_of_continuousWithinAt
- isSaddlePointOn_iff'
- sInf_mem_of_not_isPredPrelimit
- lt_biSup_iff
- Pi.Lex.le_sSup_apply
Ancestors49
- BiheytingAlgebra
- Bot
- BoundedOrder
- ChainCompletePartialOrder
- CoheytingAlgebra
- Compl
- CompleteDistribLattice
- CompleteLattice
- CompletePartialOrder
- CompleteSemilatticeInf
- CompleteSemilatticeSup
- CompletelyDistribLattice
- ConditionallyCompleteLattice
- ConditionallyCompleteLinearOrder
- ConditionallyCompleteLinearOrderBot
- ConditionallyCompletePartialOrder
- ConditionallyCompletePartialOrderInf
- ConditionallyCompletePartialOrderSup
- DistribLattice
- GeneralizedCoheytingAlgebra
- GeneralizedHeytingAlgebra
- GradeBoundedOrder
- GradeMaxOrder
- GradeMinOrder
- GradeOrder
- HImp
- HNot
- HeytingAlgebra
- InfSet
- LE
- LT
- Lattice
- LinearOrder
- Max
- Min
- Nonempty
- OmegaCompletePartialOrder
- Ord
- Order.Coframe
- Order.Frame
- OrderBot
- OrderTop
- PartialOrder
- Preorder
- SDiff
- SemilatticeInf
- SemilatticeSup
- SupSet
- Top