mathlib documentation

topology.order.lattice

Topological lattices #

In this file we define mixin classes has_continuous_inf and has_continuous_sup. We define the class topological_lattice as a topological space and lattice L extending has_continuous_inf and has_continuous_sup.

References #

Tags #

topological, lattice

@[class]
structure has_continuous_inf (L : Type u_1) [topological_space L] [has_inf L] :
Prop

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
@[class]
structure has_continuous_sup (L : Type u_1) [topological_space L] [has_sup L] :
Prop

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
@[protected, instance]

Let L be a topological space with a supremum. If the order dual has a continuous infimum then the supremum is continuous.

@[class]
structure topological_lattice (L : Type u_1) [topological_space L] [lattice L] :
Type

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.

Instances
@[continuity]
theorem continuous_inf {L : Type u_1} [topological_space L] [has_inf L] [has_continuous_inf L] :
continuous (λ (p : L × L), p.fst p.snd)
@[continuity]
theorem continuous.inf {L : Type u_1} [topological_space L] {X : Type u_2} [topological_space X] [has_inf L] [has_continuous_inf L] {f g : X → L} (hf : continuous f) (hg : continuous g) :
continuous (λ (x : X), f x g x)
@[continuity]
theorem continuous_sup {L : Type u_1} [topological_space L] [has_sup L] [has_continuous_sup L] :
continuous (λ (p : L × L), p.fst p.snd)
@[continuity]
theorem continuous.sup {L : Type u_1} [topological_space L] {X : Type u_2} [topological_space X] [has_sup L] [has_continuous_sup L] {f g : X → L} (hf : continuous f) (hg : continuous g) :
continuous (λ (x : X), f x g x)