Structures · Order
SemilatticeInf
A SemilatticeInf is a meet-semilattice, that is, a partial order
with a meet (a.k.a. glb / greatest lower bound, inf / infimum) operation
⊓ which is the greatest element smaller than both factors.
- Defined in
- Mathlib.Order.Lattice
- Shape
- One type argument · adds inf, inf_le_left, inf_le_right, le_inf
Extends1
Extended by1
Forgetful instances
Every SemilatticeInf is also a
Concrete types that are instances56
- Real
- Rat
- NNReal
- Filter.Germ
- BoundedContinuousFunction
- MeasureTheory.SimpleFunc
- Finsupp
- DFinsupp
- Tropical
- AlgebraicGeometry.Scheme.IdealSheafData
- CompactlySupportedContinuousMap
- WithTopology
- Partition
- Finpartition
- LinearPMap
- ClosedSubmodule
- TwoSidedIdeal
- CategoryTheory.Subobject
- Nucleus
- TopologicalSpace.CompactOpens
- GroupTopology
- AddGroupTopology
- Concept
- OpenSubgroup
- OpenAddSubgroup
- Booleanisation
- OpenNormalAddSubgroup
- OpenNormalSubgroup
- FiniteIndexNormalSubgroup
- FiniteIndexNormalAddSubgroup
- ClosedSubgroup
- ClosedAddSubgroup
- Graph
- DiscreteQuotient
- TopHom
- BotHom
- InfHom
- BoxIntegral.Prepartition
- InfTopHom
- PEquiv
- CategoryTheory.GrothendieckTopology.Cover
- Geometry.SimplicialComplex
- RootedTree.α
- Module.Baer.ExtensionOf
- SemilatInfCat.X
- Subtype
- Prod
- OrderDual
- Set.Elem
- ULift
- Lex
- ContinuousMap
- WithTop
- WithBot
- WithZero
- OrderHom
How is a type an instance?
Loading the hierarchy index…
Assumed by726
- inf_le_left
- inf_le_right
- Finset.inf
- inf_of_le_left
- inf_comm
- inf_of_le_right
- Finset.inf'
- le_inf
- disjoint_iff
- inf_eq_right
- disjoint_iff_inf_le
- Finset.hasInfs
- InfClosed
- inf_le_inf
- inf_assoc
- Disjoint.eq_bot
- Disjoint.le_bot
- le_inf_iff
- Set.hasInfs
- inf_eq_left
- GaloisConnection.u_inf
- inf_idem
- CategoryTheory.Pairwise.diagram
- inf_top_eq
- top_inf_eq
- InfIrred
- InfPrime
- inf_le_inf_left
- Finset.inf_le
- inf_le_inf_right
- Set.Intersecting
- infClosure
- Finset.truncatedInf
- Finset.inf'_congr
- Multiset.inf
- Monotone.map_inf_le
- OrderIso.map_inf
- inf_le_of_left_le
- Finset.inf_insert
- Finset.inf_cons
- Finset.inf_empty
- Finset.inf'_le
- inf_bot_eq
- inf_inf_inf_comm
- PrimitiveSpectrum.hull
- Finset.coe_inf'
- Finset.le_inf_iff
- Finset.inf'_eq_inf
- bot_inf_eq
- Finset.le_inf