mathlib3 documentation

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.

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 of this typeclass
@[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 of this typeclass
@[class]
structure topological_lattice (L : Type u_1) [topological_space L] [lattice L] :

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
@[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)
theorem filter.tendsto.sup_right_nhds' {ι : Type u_1} {β : Type u_2} [topological_space β] [has_sup β] [has_continuous_sup β] {l : filter ι} {f g : ι β} {x y : β} (hf : filter.tendsto f l (nhds x)) (hg : filter.tendsto g l (nhds y)) :
filter.tendsto (f g) l (nhds (x y))
theorem filter.tendsto.sup_right_nhds {ι : Type u_1} {β : Type u_2} [topological_space β] [has_sup β] [has_continuous_sup β] {l : filter ι} {f g : ι β} {x y : β} (hf : filter.tendsto f l (nhds x)) (hg : filter.tendsto g l (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} [topological_space β] [has_inf β] [has_continuous_inf β] {l : filter ι} {f g : ι β} {x y : β} (hf : filter.tendsto f l (nhds x)) (hg : filter.tendsto g l (nhds y)) :
filter.tendsto (f g) l (nhds (x y))
theorem filter.tendsto.inf_right_nhds {ι : Type u_1} {β : Type u_2} [topological_space β] [has_inf β] [has_continuous_inf β] {l : filter ι} {f g : ι β} {x y : β} (hf : filter.tendsto f l (nhds x)) (hg : filter.tendsto g l (nhds y)) :
filter.tendsto (λ (i : ι), f i g i) l (nhds (x y))