Structures · Order
SemilatticeSup
A SemilatticeSup is a join-semilattice, that is, a partial order
with a join (a.k.a. lub / least upper bound, sup / supremum) operation
⊔ which is the least element larger than both factors.
- Defined in
- Mathlib.Order.Lattice
- Shape
- One type argument · adds sup, le_sup_left, le_sup_right, sup_le
Extends1
Extended by2
Forgetful instances
Every SemilatticeSup is also a
Concrete types that are instances57
- Real
- Rat
- NNReal
- ENNReal
- Filter.Germ
- BoundedContinuousFunction
- NonemptyInterval
- MeasureTheory.SimpleFunc
- Finsupp
- Interval
- DFinsupp
- TopologicalSpace.NonemptyCompacts
- Tropical
- CompactlySupportedContinuousMap
- TopologicalSpace.Compacts
- WithTopology
- PrimeMultiset
- Seminorm
- ClosedSubmodule
- TwoSidedIdeal
- CategoryTheory.Subobject
- GroupSeminorm
- AddGroupSeminorm
- TopologicalSpace.CompactOpens
- Concept
- Booleanisation
- OpenNormalAddSubgroup
- OpenNormalSubgroup
- FiniteIndexNormalSubgroup
- FiniteIndexNormalAddSubgroup
- ValuationSubring
- Semiquot
- AddGroupNorm
- GroupNorm
- TopHom
- BotHom
- NonarchAddGroupSeminorm
- TopologicalSpace.PositiveCompacts
- SupHom
- BoxIntegral.Box
- NonarchAddGroupNorm
- SupBotHom
- ManyOneDegree
- PseudoMetric
- CategoryTheory.Coverage
- SemilatSupCat.X
- Subtype
- Prod
- OrderDual
- Set.Elem
- ULift
- Lex
- ContinuousMap
- WithTop
- WithBot
- WithZero
- OrderHom
How is a type an instance?
Loading the hierarchy index…
Assumed by867
- Finset.sup
- le_sup_left
- le_sup_right
- sup_of_le_left
- Finset.sup'
- sup_comm
- sup_le
- sup_of_le_right
- Finset.le_sup
- GaloisConnection.l_sup
- Finset.sup_empty
- sup_eq_left
- partialSups
- Finset.hasSups
- sup_le_iff
- SupClosed
- codisjoint_iff
- sup_eq_right
- AddMonoidAlgebra.supDegree
- sup_le_sup
- Finset.sup_le
- Set.hasSups
- Finset.sup_singleton
- Finset.sup'_congr
- OrderIso.map_sup
- sup_assoc
- Finset.sup'_eq_sup
- Finset.sup_insert
- SupIrred
- supClosure
- bot_sup_eq
- sup_bot_eq
- Finset.sup_cons
- sup_idem
- Finset.sup_image
- le_sup_of_le_left
- Finset.sup_mono
- Finset.sup_le_iff
- Finset.le_sup'
- Codisjoint.eq_top
- Finset.disjSups
- sup_le_sup_left
- Multiset.sup
- Filter.Tendsto.cauchySeq
- SupPrime
- Finset.truncatedSup
- le_sup_of_le_right
- Finset.sup'_le
- codisjoint_iff_le_sup
- sup_le_sup_right