# mathlib3documentation

topology.order.lattice

# Topological lattices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

## Tags #

topological, lattice

@[class]
structure has_continuous_inf (L : Type u_1) [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 of this typeclass
@[class]
structure has_continuous_sup (L : Type u_1) [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 of this typeclass
@[protected, instance]
@[protected, instance]
@[class]
structure topological_lattice (L : Type u_1) [lattice L] :
• to_has_continuous_inf :
• to_has_continuous_sup :

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 of this typeclass
Instances of other typeclasses for topological_lattice
• topological_lattice.has_sizeof_inst
@[protected, instance]
Equations
@[protected, instance]
Equations
@[continuity]
theorem continuous_inf {L : Type u_1} [has_inf L]  :
continuous (λ (p : L × L), p.fst p.snd)
@[continuity]
theorem continuous.inf {L : Type u_1} {X : Type u_2} [has_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} [has_sup L]  :
continuous (λ (p : L × L), p.fst p.snd)
@[continuity]
theorem continuous.sup {L : Type u_1} {X : Type u_2} [has_sup L] {f g : X L} (hf : continuous f) (hg : continuous g) :
continuous (λ (x : X), f x g x)
theorem filter.tendsto.sup_right_nhds' {ι : Type u_1} {β : Type u_2} [has_sup β] {l : filter ι} {f g : ι β} {x y : β} (hf : (nhds x)) (hg : (nhds y)) :
filter.tendsto (f g) l (nhds (x y))
theorem filter.tendsto.sup_right_nhds {ι : Type u_1} {β : Type u_2} [has_sup β] {l : filter ι} {f g : ι β} {x y : β} (hf : (nhds x)) (hg : (nhds y)) :
filter.tendsto (λ (i : ι), f i g i) l (nhds (x y))
theorem filter.tendsto.inf_right_nhds' {ι : Type u_1} {β : Type u_2} [has_inf β] {l : filter ι} {f g : ι β} {x y : β} (hf : (nhds x)) (hg : (nhds y)) :
filter.tendsto (f g) l (nhds (x y))
theorem filter.tendsto.inf_right_nhds {ι : Type u_1} {β : Type u_2} [has_inf β] {l : filter ι} {f g : ι β} {x y : β} (hf : (nhds x)) (hg : (nhds y)) :
filter.tendsto (λ (i : ι), f i g i) l (nhds (x y))