Structures · Topology
TopologicalLattice
Let L be a lattice equipped with a topology such that L has continuous infimum and supremum.
Then L is said to be a topological lattice.
- Defined in
- Mathlib.Topology.Order.Lattice
- Shape
- One type argument
Extends2
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- OrderDual
How is a type an instance?
Loading the hierarchy index…
Assumed by11
- MeasureTheory.AEEqFun.coeFn_abs
- ContinuousMap.instLatticeOfTopologicalLattice
- TopologicalLattice.toContinuousInf
- ContinuousMap.mabs_apply
- TopologicalLattice.toContinuousSup
- OrderDual.topologicalLattice
- CompactlySupportedContinuousMap.instLatticeOfTopologicalLattice
- ContinuousMap.coe_mabs
- ContinuousMap.abs_apply
- ContinuousMap.coe_abs
- MeasureTheory.AEEqFun.instLattice