Structures · Order
CompleteLattice
A complete lattice is a bounded lattice which has suprema and infima for every subset.
- Defined in
- Mathlib.Order.CompleteLattice.Defs
- Shape
- One type argument · adds isLUB_sSup, isGLB_sInf
Extends4
Extended by5
Forgetful instances
Every CompleteLattice is also a
Concrete types that are instances86
- Interval
- UpperSet
- LowerSet
- LieSubalgebra
- LieSubmodule
- AlgebraicGeometry.Scheme.IdealSheafData
- MeasureTheory.Measure
- TopologicalSpace.Opens
- AddSubgroup
- AddSubmonoid
- NonUnitalSubalgebra
- NonUnitalStarSubalgebra
- Sublattice
- BooleanSubalgebra
- UniformSpace
- TopologicalSpace
- TopologicalSpace.Closeds
- RingCon
- SimpleGraph.Subgraph
- MeasureTheory.OuterMeasure
- SubMulAction
- ConvexCone
- StarSubalgebra
- ClosedSubmodule
- TwoSidedIdeal
- HomogeneousIdeal
- AffineSubspace
- Class
- NonUnitalSubring
- CategoryTheory.Subobject
- Sublocale
- NonUnitalSubsemiring
- Nucleus
- SubAddAction
- SaturatedAddSubmonoid
- AddSubsemigroup
- SaturatedSubmonoid
- Order.Ideal
- StructureGroupoid
- CategoryTheory.Subgroupoid
- FirstOrder.Language.Substructure
- DividedPowers.SubDPIdeal
- AbstractSimplicialComplex
- PreAbstractSimplicialComplex
- Projectivization.Subspace
- CategoryTheory.GrothendieckTopology
- CategoryTheory.Sieve
- CategoryTheory.Pretopology
- MeasureTheory.Filtration
- CategoryTheory.Precoverage
- Ideal.Filtration
- GroupTopology
- RingTopology
- AddGroupTopology
- Concept
- MeasurableSpace
- CategoryTheory.SubmonoidFunctor
- CategoryTheory.Subfunctor
- Setoid
- PresheafOfModules.Submodule
- CategoryTheory.Presieve
- Setoid.Partitions
- CompleteLat.carrier
- DiffeologicalSpace
- Subtype
- Prod
- OrderDual
- Set.Elem
- ULift
- Lex
- WithTop
- WithBot
- Colex
- Submodule
- Filter
- Subgroup
- OrderHom
- IntermediateField
- Subalgebra
- Subfield
- Submonoid
- Subring
- Subsemiring
- Subsemigroup
- AddCon
- Con
How is a type an instance?
Loading the hierarchy index…
Assumed by1,150
- le_iSup
- iSup_le
- iInf_le
- le_iInf
- iSupIndep
- iSup₂_le
- le_iSup_of_le
- GaloisConnection.l_iSup
- le_iInf₂
- iInf_le_of_le
- iSup_pos
- le_iSup₂
- le_iSup₂_of_le
- iSup_neg
- iInf₂_le
- iSup_le_iff
- iSup_subtype'
- sSup_eq_iSup
- GaloisConnection.u_iInf
- sSupIndep
- iSup_mono
- sSup_image
- iInf_subtype'
- iInf_pos
- le_iInf_iff
- Finset.sup_eq_iSup
- iSup_bot
- iInf₂_le_of_le
- iInf_mono
- iInf_neg
- iInf_range
- iSup_subtype
- OrderIso.map_iInf
- sInf_image
- OrderIso.map_iSup
- iSup_range
- OrdinalApprox.gfpApprox
- sInf_eq_iInf
- iInf_top
- OrdinalApprox.lfpApprox
- le_biSup
- CompleteLattice.MulticoequalizerDiagram.multispanIndex
- iSup₂_le_iff
- sSup_empty
- Finset.inf_eq_iInf
- GaloisConnection.l_sSup
- inf_eq_iInf
- iSup₂_mono
- iSup_subtype''
- OrderIso.map_sSup_eq_sSup_symm_preimage
Ancestors30
- Bot
- BoundedOrder
- ChainCompletePartialOrder
- CompletePartialOrder
- CompleteSemilatticeInf
- CompleteSemilatticeSup
- ConditionallyCompleteLattice
- ConditionallyCompletePartialOrder
- ConditionallyCompletePartialOrderInf
- ConditionallyCompletePartialOrderSup
- GradeBoundedOrder
- GradeMaxOrder
- GradeMinOrder
- GradeOrder
- InfSet
- LE
- LT
- Lattice
- Max
- Min
- Nonempty
- OmegaCompletePartialOrder
- OrderBot
- OrderTop
- PartialOrder
- Preorder
- SemilatticeInf
- SemilatticeSup
- SupSet
- Top