Structures · Order
Lattice
A lattice is a join-semilattice which is also a meet-semilattice.
- Defined in
- Mathlib.Order.Lattice
- Shape
- One type argument · adds inf, inf_le_left, inf_le_right, le_inf
Extends2
Extended by6
Forgetful instances
Provided automatically by
Concrete types that are instances53
- Int
- Nat
- Real
- Rat
- Filter.Germ
- BoundedContinuousFunction
- MeasureTheory.SimpleFunc
- Finsupp
- Lat.carrier
- Interval
- DFinsupp
- Tropical
- FractionalIdeal
- MeasureTheory.AEEqFun
- Associates
- CompactlySupportedContinuousMap
- WithTopology
- Function.locallyFinsuppWithin
- Seminorm
- ClosedSubmodule
- CategoryTheory.Subobject
- GroupSeminorm
- AddGroupSeminorm
- Order.Ideal
- CircleDeg1Lift
- Concept
- OpenSubgroup
- OpenAddSubgroup
- Heyting.Regular
- OpenNormalAddSubgroup
- OpenNormalSubgroup
- FiniteIndexNormalSubgroup
- FiniteIndexNormalAddSubgroup
- FiniteGaloisIntermediateField
- ClopenUpperSet
- Subrepresentation
- TopHom
- BotHom
- TopologicalSpace.OpenNhds
- Subtype
- Prod
- OrderDual
- Set.Elem
- ULift
- Fin
- Lex
- ContinuousMap
- WithTop
- WithBot
- WithZero
- Multiset
- Finset
- OrderHom
How is a type an instance?
Loading the hierarchy index…
Assumed by1,065
- abs
- Set.uIcc
- abs_of_nonneg
- Finpartition.parts
- abs_nonneg
- mabs
- abs_of_pos
- le_abs_self
- abs_neg
- abs_zero
- Finset.uIcc
- Set.uIcc_of_le
- abs_of_nonpos
- Finset.SupIndep
- abs_sub_comm
- CompositionSeries
- abs_of_neg
- Nat.abs_cast
- LatticeHom.toSupHom
- BoundedLatticeHom.comp
- LatticeHom.comp
- latticeClosure
- Sublattice.carrier
- IsComplemented
- Set.uIcc_of_ge
- IsCompl.sup_eq_top
- Sublattice.map
- BoundedLatticeHom.id
- abs_abs
- Lattice.inf
- Set.uIcc_comm
- Sublattice.prod
- neg_le_abs
- LatticeHom.id
- Sublattice.comap
- Set.left_mem_uIcc
- abs_add_le
- IsSublattice.infClosed
- Finpartition.sup_parts
- IsSublattice.supClosed
- Finpartition.le
- inf_le_sup
- Finset.coe_uIcc
- Finpartition.disjoint
- mabs_inv
- JordanHolderLattice.Iso
- Set.right_mem_uIcc
- Lattice.inf_le_right
- posPart_zero
- Lattice.inf_le_left