# Topological lattices #

In this file we define mixin classes `ContinuousInf`

and `ContinuousSup`

. We define the
class `TopologicalLattice`

as a topological space and lattice `L`

extending `ContinuousInf`

and
`ContinuousSup`

.

## References #

- [Gierz et al, A Compendium of Continuous Lattices][GierzEtAl1980]

## Tags #

topological, lattice

- continuous_inf : Continuous fun p => p.fst ⊓ p.snd
The infimum is continuous

Let `L`

be a topological space and let `L×L`

be equipped with the product topology and let
`⊓:L×L → L`

be an infimum. Then `L`

is said to have *(jointly) continuous infimum* if the map
`⊓:L×L → L`

is continuous.

## Instances

- continuous_sup : Continuous fun p => p.fst ⊔ p.snd
The supremum is continuous

Let `L`

be a topological space and let `L×L`

be equipped with the product topology and let
`⊓:L×L → L`

be a supremum. Then `L`

is said to have *(jointly) continuous supremum* if the map
`⊓:L×L → L`

is continuous.

## Instances

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*.