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

## Tags #

topological, lattice

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

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.

• continuous_inf : Continuous fun (p : L × L) => p.1 p.2

The infimum is continuous

Instances
theorem ContinuousInf.continuous_inf {L : Type u_1} [] [Inf L] [self : ] :
Continuous fun (p : L × L) => p.1 p.2

The infimum is continuous

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

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.

• continuous_sup : Continuous fun (p : L × L) => p.1 p.2

The supremum is continuous

Instances
theorem ContinuousSup.continuous_sup {L : Type u_1} [] [Sup L] [self : ] :
Continuous fun (p : L × L) => p.1 p.2

The supremum is continuous

@[instance 100]
instance OrderDual.continuousSup (L : Type u_1) [] [Inf L] [] :
Equations
• =
@[instance 100]
instance OrderDual.continuousInf (L : Type u_1) [] [Sup L] [] :
Equations
• =
class TopologicalLattice (L : Type u_1) [] [] extends , :

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
@[instance 100]
instance OrderDual.topologicalLattice (L : Type u_1) [] [] :
Equations
• =
@[instance 100]
instance LinearOrder.topologicalLattice {L : Type u_1} [] [] :
Equations
• =
theorem continuous_inf {L : Type u_1} [] [Inf L] [] :
Continuous fun (p : L × L) => p.1 p.2
theorem Continuous.inf {L : Type u_1} {X : Type u_2} [] [] [Inf L] [] {f : XL} {g : XL} (hf : ) (hg : ) :
Continuous fun (x : X) => f x g x
theorem continuous_sup {L : Type u_1} [] [Sup L] [] :
Continuous fun (p : L × L) => p.1 p.2
theorem Continuous.sup {L : Type u_1} {X : Type u_2} [] [] [Sup L] [] {f : XL} {g : XL} (hf : ) (hg : ) :
Continuous fun (x : X) => f x g x
theorem Filter.Tendsto.sup_nhds' {L : Type u_1} [] {α : Type u_3} {l : } {f : αL} {g : αL} {x : L} {y : L} [Sup L] [] (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_nhds {L : Type u_1} [] {α : Type u_3} {l : } {f : αL} {g : αL} {x : L} {y : L} [Sup L] [] (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_nhds' {L : Type u_1} [] {α : Type u_3} {l : } {f : αL} {g : αL} {x : L} {y : L} [Inf L] [] (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_nhds {L : Type u_1} [] {α : Type u_3} {l : } {f : αL} {g : αL} {x : L} {y : L} [Inf L] [] (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.finset_sup'_nhds {L : Type u_1} [] {ι : Type u_3} {α : Type u_4} {s : } {f : ιαL} {l : } {g : ιL} [] [] (hne : s.Nonempty) (hs : is, Filter.Tendsto (f i) l (nhds (g i))) :
Filter.Tendsto (s.sup' hne f) l (nhds (s.sup' hne g))
theorem Filter.Tendsto.finset_sup'_nhds_apply {L : Type u_1} [] {ι : Type u_3} {α : Type u_4} {s : } {f : ιαL} {l : } {g : ιL} [] [] (hne : s.Nonempty) (hs : is, Filter.Tendsto (f i) l (nhds (g i))) :
Filter.Tendsto (fun (a : α) => s.sup' hne fun (x : ι) => f x a) l (nhds (s.sup' hne g))
theorem Filter.Tendsto.finset_inf'_nhds {L : Type u_1} [] {ι : Type u_3} {α : Type u_4} {s : } {f : ιαL} {l : } {g : ιL} [] [] (hne : s.Nonempty) (hs : is, Filter.Tendsto (f i) l (nhds (g i))) :
Filter.Tendsto (s.inf' hne f) l (nhds (s.inf' hne g))
theorem Filter.Tendsto.finset_inf'_nhds_apply {L : Type u_1} [] {ι : Type u_3} {α : Type u_4} {s : } {f : ιαL} {l : } {g : ιL} [] [] (hne : s.Nonempty) (hs : is, Filter.Tendsto (f i) l (nhds (g i))) :
Filter.Tendsto (fun (a : α) => s.inf' hne fun (x : ι) => f x a) l (nhds (s.inf' hne g))
theorem Filter.Tendsto.finset_sup_nhds {L : Type u_1} [] {ι : Type u_3} {α : Type u_4} {s : } {f : ιαL} {l : } {g : ιL} [] [] [] (hs : is, Filter.Tendsto (f i) l (nhds (g i))) :
Filter.Tendsto (s.sup f) l (nhds (s.sup g))
theorem Filter.Tendsto.finset_sup_nhds_apply {L : Type u_1} [] {ι : Type u_3} {α : Type u_4} {s : } {f : ιαL} {l : } {g : ιL} [] [] [] (hs : is, Filter.Tendsto (f i) l (nhds (g i))) :
Filter.Tendsto (fun (a : α) => s.sup fun (x : ι) => f x a) l (nhds (s.sup g))
theorem Filter.Tendsto.finset_inf_nhds {L : Type u_1} [] {ι : Type u_3} {α : Type u_4} {s : } {f : ιαL} {l : } {g : ιL} [] [] [] (hs : is, Filter.Tendsto (f i) l (nhds (g i))) :
Filter.Tendsto (s.inf f) l (nhds (s.inf g))
theorem Filter.Tendsto.finset_inf_nhds_apply {L : Type u_1} [] {ι : Type u_3} {α : Type u_4} {s : } {f : ιαL} {l : } {g : ιL} [] [] [] (hs : is, Filter.Tendsto (f i) l (nhds (g i))) :
Filter.Tendsto (fun (a : α) => s.inf fun (x : ι) => f x a) l (nhds (s.inf g))
theorem ContinuousAt.sup' {L : Type u_1} {X : Type u_2} [] [] [Sup L] [] {f : XL} {g : XL} {x : X} (hf : ) (hg : ) :
theorem ContinuousAt.sup {L : Type u_1} {X : Type u_2} [] [] [Sup L] [] {f : XL} {g : XL} {x : X} (hf : ) (hg : ) :
ContinuousAt (fun (a : X) => f a g a) x
theorem ContinuousWithinAt.sup' {L : Type u_1} {X : Type u_2} [] [] [Sup L] [] {f : XL} {g : XL} {s : Set X} {x : X} (hf : ) (hg : ) :
theorem ContinuousWithinAt.sup {L : Type u_1} {X : Type u_2} [] [] [Sup L] [] {f : XL} {g : XL} {s : Set X} {x : X} (hf : ) (hg : ) :
ContinuousWithinAt (fun (a : X) => f a g a) s x
theorem ContinuousOn.sup' {L : Type u_1} {X : Type u_2} [] [] [Sup L] [] {f : XL} {g : XL} {s : Set X} (hf : ) (hg : ) :
theorem ContinuousOn.sup {L : Type u_1} {X : Type u_2} [] [] [Sup L] [] {f : XL} {g : XL} {s : Set X} (hf : ) (hg : ) :
ContinuousOn (fun (a : X) => f a g a) s
theorem Continuous.sup' {L : Type u_1} {X : Type u_2} [] [] [Sup L] [] {f : XL} {g : XL} (hf : ) (hg : ) :
theorem ContinuousAt.inf' {L : Type u_1} {X : Type u_2} [] [] [Inf L] [] {f : XL} {g : XL} {x : X} (hf : ) (hg : ) :
theorem ContinuousAt.inf {L : Type u_1} {X : Type u_2} [] [] [Inf L] [] {f : XL} {g : XL} {x : X} (hf : ) (hg : ) :
ContinuousAt (fun (a : X) => f a g a) x
theorem ContinuousWithinAt.inf' {L : Type u_1} {X : Type u_2} [] [] [Inf L] [] {f : XL} {g : XL} {s : Set X} {x : X} (hf : ) (hg : ) :
theorem ContinuousWithinAt.inf {L : Type u_1} {X : Type u_2} [] [] [Inf L] [] {f : XL} {g : XL} {s : Set X} {x : X} (hf : ) (hg : ) :
ContinuousWithinAt (fun (a : X) => f a g a) s x
theorem ContinuousOn.inf' {L : Type u_1} {X : Type u_2} [] [] [Inf L] [] {f : XL} {g : XL} {s : Set X} (hf : ) (hg : ) :
theorem ContinuousOn.inf {L : Type u_1} {X : Type u_2} [] [] [Inf L] [] {f : XL} {g : XL} {s : Set X} (hf : ) (hg : ) :
ContinuousOn (fun (a : X) => f a g a) s
theorem Continuous.inf' {L : Type u_1} {X : Type u_2} [] [] [Inf L] [] {f : XL} {g : XL} (hf : ) (hg : ) :
theorem ContinuousAt.finset_sup'_apply {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] {s : } {f : ιXL} {x : X} (hne : s.Nonempty) (hs : is, ContinuousAt (f i) x) :
ContinuousAt (fun (a : X) => s.sup' hne fun (x : ι) => f x a) x
theorem ContinuousAt.finset_sup' {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] {s : } {f : ιXL} {x : X} (hne : s.Nonempty) (hs : is, ContinuousAt (f i) x) :
ContinuousAt (s.sup' hne f) x
theorem ContinuousWithinAt.finset_sup'_apply {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] {s : } {f : ιXL} {t : Set X} {x : X} (hne : s.Nonempty) (hs : is, ContinuousWithinAt (f i) t x) :
ContinuousWithinAt (fun (a : X) => s.sup' hne fun (x : ι) => f x a) t x
theorem ContinuousWithinAt.finset_sup' {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] {s : } {f : ιXL} {t : Set X} {x : X} (hne : s.Nonempty) (hs : is, ContinuousWithinAt (f i) t x) :
ContinuousWithinAt (s.sup' hne f) t x
theorem ContinuousOn.finset_sup'_apply {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] {s : } {f : ιXL} {t : Set X} (hne : s.Nonempty) (hs : is, ContinuousOn (f i) t) :
ContinuousOn (fun (a : X) => s.sup' hne fun (x : ι) => f x a) t
theorem ContinuousOn.finset_sup' {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] {s : } {f : ιXL} {t : Set X} (hne : s.Nonempty) (hs : is, ContinuousOn (f i) t) :
ContinuousOn (s.sup' hne f) t
theorem Continuous.finset_sup'_apply {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] {s : } {f : ιXL} (hne : s.Nonempty) (hs : is, Continuous (f i)) :
Continuous fun (a : X) => s.sup' hne fun (x : ι) => f x a
theorem Continuous.finset_sup' {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] {s : } {f : ιXL} (hne : s.Nonempty) (hs : is, Continuous (f i)) :
Continuous (s.sup' hne f)
theorem ContinuousAt.finset_sup_apply {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] [] {s : } {f : ιXL} {x : X} (hs : is, ContinuousAt (f i) x) :
ContinuousAt (fun (a : X) => s.sup fun (x : ι) => f x a) x
theorem ContinuousAt.finset_sup {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] [] {s : } {f : ιXL} {x : X} (hs : is, ContinuousAt (f i) x) :
ContinuousAt (s.sup f) x
theorem ContinuousWithinAt.finset_sup_apply {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] [] {s : } {f : ιXL} {t : Set X} {x : X} (hs : is, ContinuousWithinAt (f i) t x) :
ContinuousWithinAt (fun (a : X) => s.sup fun (x : ι) => f x a) t x
theorem ContinuousWithinAt.finset_sup {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] [] {s : } {f : ιXL} {t : Set X} {x : X} (hs : is, ContinuousWithinAt (f i) t x) :
ContinuousWithinAt (s.sup f) t x
theorem ContinuousOn.finset_sup_apply {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] [] {s : } {f : ιXL} {t : Set X} (hs : is, ContinuousOn (f i) t) :
ContinuousOn (fun (a : X) => s.sup fun (x : ι) => f x a) t
theorem ContinuousOn.finset_sup {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] [] {s : } {f : ιXL} {t : Set X} (hs : is, ContinuousOn (f i) t) :
ContinuousOn (s.sup f) t
theorem Continuous.finset_sup_apply {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] [] {s : } {f : ιXL} (hs : is, Continuous (f i)) :
Continuous fun (a : X) => s.sup fun (x : ι) => f x a
theorem Continuous.finset_sup {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] [] {s : } {f : ιXL} (hs : is, Continuous (f i)) :
Continuous (s.sup f)
theorem ContinuousAt.finset_inf'_apply {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] {s : } {f : ιXL} {x : X} (hne : s.Nonempty) (hs : is, ContinuousAt (f i) x) :
ContinuousAt (fun (a : X) => s.inf' hne fun (x : ι) => f x a) x
theorem ContinuousAt.finset_inf' {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] {s : } {f : ιXL} {x : X} (hne : s.Nonempty) (hs : is, ContinuousAt (f i) x) :
ContinuousAt (s.inf' hne f) x
theorem ContinuousWithinAt.finset_inf'_apply {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] {s : } {f : ιXL} {t : Set X} {x : X} (hne : s.Nonempty) (hs : is, ContinuousWithinAt (f i) t x) :
ContinuousWithinAt (fun (a : X) => s.inf' hne fun (x : ι) => f x a) t x
theorem ContinuousWithinAt.finset_inf' {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] {s : } {f : ιXL} {t : Set X} {x : X} (hne : s.Nonempty) (hs : is, ContinuousWithinAt (f i) t x) :
ContinuousWithinAt (s.inf' hne f) t x
theorem ContinuousOn.finset_inf'_apply {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] {s : } {f : ιXL} {t : Set X} (hne : s.Nonempty) (hs : is, ContinuousOn (f i) t) :
ContinuousOn (fun (a : X) => s.inf' hne fun (x : ι) => f x a) t
theorem ContinuousOn.finset_inf' {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] {s : } {f : ιXL} {t : Set X} (hne : s.Nonempty) (hs : is, ContinuousOn (f i) t) :
ContinuousOn (s.inf' hne f) t
theorem Continuous.finset_inf'_apply {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] {s : } {f : ιXL} (hne : s.Nonempty) (hs : is, Continuous (f i)) :
Continuous fun (a : X) => s.inf' hne fun (x : ι) => f x a
theorem Continuous.finset_inf' {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] {s : } {f : ιXL} (hne : s.Nonempty) (hs : is, Continuous (f i)) :
Continuous (s.inf' hne f)
theorem ContinuousAt.finset_inf_apply {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] [] {s : } {f : ιXL} {x : X} (hs : is, ContinuousAt (f i) x) :
ContinuousAt (fun (a : X) => s.inf fun (x : ι) => f x a) x
theorem ContinuousAt.finset_inf {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] [] {s : } {f : ιXL} {x : X} (hs : is, ContinuousAt (f i) x) :
ContinuousAt (s.inf f) x
theorem ContinuousWithinAt.finset_inf_apply {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] [] {s : } {f : ιXL} {t : Set X} {x : X} (hs : is, ContinuousWithinAt (f i) t x) :
ContinuousWithinAt (fun (a : X) => s.inf fun (x : ι) => f x a) t x
theorem ContinuousWithinAt.finset_inf {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] [] {s : } {f : ιXL} {t : Set X} {x : X} (hs : is, ContinuousWithinAt (f i) t x) :
ContinuousWithinAt (s.inf f) t x
theorem ContinuousOn.finset_inf_apply {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] [] {s : } {f : ιXL} {t : Set X} (hs : is, ContinuousOn (f i) t) :
ContinuousOn (fun (a : X) => s.inf fun (x : ι) => f x a) t
theorem ContinuousOn.finset_inf {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] [] {s : } {f : ιXL} {t : Set X} (hs : is, ContinuousOn (f i) t) :
ContinuousOn (s.inf f) t
theorem Continuous.finset_inf_apply {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] [] {s : } {f : ιXL} (hs : is, Continuous (f i)) :
Continuous fun (a : X) => s.inf fun (x : ι) => f x a
theorem Continuous.finset_inf {L : Type u_1} {X : Type u_2} [] [] {ι : Type u_3} [] [] [] {s : } {f : ιXL} (hs : is, Continuous (f i)) :
Continuous (s.inf f)