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 #

Gierz et al, A Compendium of Continuous Lattices

Tags #

topological, lattice

source

@[class]

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

Prop

continuous_inf : continuous (λ (p : L × L), p.fst ⊓ p.snd)

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

source

@[class]

structure has_continuous_sup (L : Type u_1) [topological_space L] [has_sup L] :

Prop

continuous_sup : continuous (λ (p : L × L), p.fst ⊔ p.snd)

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

source

@[protected, instance]

def order_dual.has_continuous_sup (L : Type u_1) [topological_space L] [has_inf L] [has_continuous_inf L] :

has_continuous_sup Lᵒᵈ

source

@[protected, instance]

def order_dual.has_continuous_inf (L : Type u_1) [topological_space L] [has_sup L] [has_continuous_sup L] :

has_continuous_inf Lᵒᵈ

source

@[class]

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

Type

to_has_continuous_inf : has_continuous_inf L
to_has_continuous_sup : has_continuous_sup 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

source

@[protected, instance]

def order_dual.topological_lattice (L : Type u_1) [topological_space L] [lattice L] [topological_lattice L] :

topological_lattice Lᵒᵈ

Equations

order_dual.topological_lattice L = topological_lattice.mk

source

@[protected, instance]

def linear_order.topological_lattice {L : Type u_1} [topological_space L] [linear_order L] [order_closed_topology L] :

topological_lattice L

Equations

linear_order.topological_lattice = topological_lattice.mk

source

@[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)

source

@[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)

source

@[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)

source

@[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)

source

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))

source

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))

source

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))

source

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))