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

class ContinuousInf (L : Type u_1) [TopologicalSpace L] [Inf L] : Prop

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

class ContinuousSup (L : Type u_1) [TopologicalSpace L] [Sup L] : Prop

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

instance OrderDual.continuousSup (L : Type u_1) [TopologicalSpace L] [Inf L] [ContinuousInf L] : ContinuousSup Lᵒᵈ

Equations

• OrderDual.continuousSup = OrderDual.continuousSup.proof_1

instance OrderDual.continuousInf (L : Type u_1) [TopologicalSpace L] [Sup L] [ContinuousSup L] : ContinuousInf Lᵒᵈ

Equations

• OrderDual.continuousInf = OrderDual.continuousInf.proof_1

class TopologicalLattice (L : Type u_1) [TopologicalSpace L] [Lattice L] extends ContinuousInf , ContinuousSup : Prop

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.

instance OrderDual.topologicalLattice (L : Type u_1) [TopologicalSpace L] [Lattice L] [TopologicalLattice L] : TopologicalLattice Lᵒᵈ

Equations

• OrderDual.topologicalLattice = OrderDual.topologicalLattice.proof_1

instance LinearOrder.topologicalLattice {L : Type u_1} [TopologicalSpace L] [LinearOrder L] [OrderClosedTopology L] : TopologicalLattice L

Equations

• @LinearOrder.topologicalLattice = @LinearOrder.topologicalLattice.proof_1

theorem continuous_inf {L : Type u_1} [TopologicalSpace L] [Inf L] [ContinuousInf L] : Continuous fun p => p.fst ⊓ p.snd

theorem Continuous.inf {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] [Inf L] [ContinuousInf L] {f : X → L} {g : X → L} (hf : Continuous f) (hg : Continuous g) : Continuous fun x => f x ⊓ g x

theorem continuous_sup {L : Type u_1} [TopologicalSpace L] [Sup L] [ContinuousSup L] : Continuous fun p => p.fst ⊔ p.snd

theorem Continuous.sup {L : Type u_1} {X : Type u_2} [TopologicalSpace L] [TopologicalSpace X] [Sup L] [ContinuousSup L] {f : X → L} {g : X → L} (hf : Continuous f) (hg : Continuous g) : Continuous fun x => f x ⊔ g x

theorem Filter.Tendsto.sup_right_nhds' {ι : Type u_1} {β : Type u_2} [TopologicalSpace β] [Sup β] [ContinuousSup β] {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} [TopologicalSpace β] [Sup β] [ContinuousSup β] {l : Filter ι} {f : ι → β} {g : ι → β} {x : β} {y : β} (hf : Filter.Tendsto f l (nhds x)) (hg : Filter.Tendsto g l (nhds y)) : Filter.Tendsto (fun i => f i ⊔ g i) l (nhds (x ⊔ y))

theorem Filter.Tendsto.inf_right_nhds' {ι : Type u_1} {β : Type u_2} [TopologicalSpace β] [Inf β] [ContinuousInf β] {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} [TopologicalSpace β] [Inf β] [ContinuousInf β] {l : Filter ι} {f : ι → β} {g : ι → β} {x : β} {y : β} (hf : Filter.Tendsto f l (nhds x)) (hg : Filter.Tendsto g l (nhds y)) : Filter.Tendsto (fun i => f i ⊓ g i) l (nhds (x ⊓ y))