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
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}
:
∀ {inst : TopologicalSpace L} {inst_1 : Inf L} [self : ContinuousInf L], Continuous fun (p : L × L) => p.1 ⊓ p.2
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 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}
:
∀ {inst : TopologicalSpace L} {inst_1 : Sup L} [self : ContinuousSup L], Continuous fun (p : L × L) => p.1 ⊔ p.2
The supremum is continuous
@[instance 100]
Equations
- ⋯ = ⋯
@[instance 100]
Equations
- ⋯ = ⋯
class
TopologicalLattice
(L : Type u_1)
[TopologicalSpace L]
[Lattice L]
extends
ContinuousInf
,
ContinuousSup
:
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)
[TopologicalSpace L]
[Lattice L]
[TopologicalLattice L]
:
Equations
- ⋯ = ⋯
@[instance 100]
instance
LinearOrder.topologicalLattice
{L : Type u_1}
[TopologicalSpace L]
[LinearOrder L]
[OrderClosedTopology L]
:
Equations
- ⋯ = ⋯
theorem
continuous_inf
{L : Type u_1}
[TopologicalSpace L]
[Inf L]
[ContinuousInf L]
:
Continuous fun (p : L × L) => p.1 ⊓ p.2
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 : X) => f x ⊓ g x
theorem
continuous_sup
{L : Type u_1}
[TopologicalSpace L]
[Sup L]
[ContinuousSup L]
:
Continuous fun (p : L × L) => p.1 ⊔ p.2
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 : X) => f x ⊔ g x
theorem
Filter.Tendsto.sup_nhds'
{L : Type u_1}
[TopologicalSpace L]
{α : Type u_3}
{l : Filter α}
{f : α → L}
{g : α → L}
{x : L}
{y : L}
[Sup L]
[ContinuousSup 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}
[TopologicalSpace L]
{α : Type u_3}
{l : Filter α}
{f : α → L}
{g : α → L}
{x : L}
{y : L}
[Sup L]
[ContinuousSup 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}
[TopologicalSpace L]
{α : Type u_3}
{l : Filter α}
{f : α → L}
{g : α → L}
{x : L}
{y : L}
[Inf L]
[ContinuousInf 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}
[TopologicalSpace L]
{α : Type u_3}
{l : Filter α}
{f : α → L}
{g : α → L}
{x : L}
{y : L}
[Inf L]
[ContinuousInf 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}
[TopologicalSpace L]
{ι : Type u_3}
{α : Type u_4}
{s : Finset ι}
{f : ι → α → L}
{l : Filter α}
{g : ι → L}
[SemilatticeSup L]
[ContinuousSup L]
(hne : s.Nonempty)
(hs : ∀ i ∈ s, 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}
[TopologicalSpace L]
{ι : Type u_3}
{α : Type u_4}
{s : Finset ι}
{f : ι → α → L}
{l : Filter α}
{g : ι → L}
[SemilatticeSup L]
[ContinuousSup L]
(hne : s.Nonempty)
(hs : ∀ i ∈ s, 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}
[TopologicalSpace L]
{ι : Type u_3}
{α : Type u_4}
{s : Finset ι}
{f : ι → α → L}
{l : Filter α}
{g : ι → L}
[SemilatticeInf L]
[ContinuousInf L]
(hne : s.Nonempty)
(hs : ∀ i ∈ s, 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}
[TopologicalSpace L]
{ι : Type u_3}
{α : Type u_4}
{s : Finset ι}
{f : ι → α → L}
{l : Filter α}
{g : ι → L}
[SemilatticeInf L]
[ContinuousInf L]
(hne : s.Nonempty)
(hs : ∀ i ∈ s, 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}
[TopologicalSpace L]
{ι : Type u_3}
{α : Type u_4}
{s : Finset ι}
{f : ι → α → L}
{l : Filter α}
{g : ι → L}
[SemilatticeSup L]
[OrderBot L]
[ContinuousSup L]
(hs : ∀ i ∈ s, 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}
[TopologicalSpace L]
{ι : Type u_3}
{α : Type u_4}
{s : Finset ι}
{f : ι → α → L}
{l : Filter α}
{g : ι → L}
[SemilatticeSup L]
[OrderBot L]
[ContinuousSup L]
(hs : ∀ i ∈ s, 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}
[TopologicalSpace L]
{ι : Type u_3}
{α : Type u_4}
{s : Finset ι}
{f : ι → α → L}
{l : Filter α}
{g : ι → L}
[SemilatticeInf L]
[OrderTop L]
[ContinuousInf L]
(hs : ∀ i ∈ s, 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}
[TopologicalSpace L]
{ι : Type u_3}
{α : Type u_4}
{s : Finset ι}
{f : ι → α → L}
{l : Filter α}
{g : ι → L}
[SemilatticeInf L]
[OrderTop L]
[ContinuousInf L]
(hs : ∀ i ∈ s, 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}
[TopologicalSpace L]
[TopologicalSpace X]
[Sup L]
[ContinuousSup L]
{f : X → L}
{g : X → L}
{x : X}
(hf : ContinuousAt f x)
(hg : ContinuousAt g x)
:
ContinuousAt (f ⊔ g) x
theorem
ContinuousAt.sup
{L : Type u_1}
{X : Type u_2}
[TopologicalSpace L]
[TopologicalSpace X]
[Sup L]
[ContinuousSup L]
{f : X → L}
{g : X → L}
{x : X}
(hf : ContinuousAt f x)
(hg : ContinuousAt g x)
:
ContinuousAt (fun (a : X) => f a ⊔ g a) x
theorem
ContinuousWithinAt.sup'
{L : Type u_1}
{X : Type u_2}
[TopologicalSpace L]
[TopologicalSpace X]
[Sup L]
[ContinuousSup L]
{f : X → L}
{g : X → L}
{s : Set X}
{x : X}
(hf : ContinuousWithinAt f s x)
(hg : ContinuousWithinAt g s x)
:
ContinuousWithinAt (f ⊔ g) s x
theorem
ContinuousWithinAt.sup
{L : Type u_1}
{X : Type u_2}
[TopologicalSpace L]
[TopologicalSpace X]
[Sup L]
[ContinuousSup L]
{f : X → L}
{g : X → L}
{s : Set X}
{x : X}
(hf : ContinuousWithinAt f s x)
(hg : ContinuousWithinAt g s x)
:
ContinuousWithinAt (fun (a : X) => f a ⊔ g a) s x
theorem
ContinuousOn.sup'
{L : Type u_1}
{X : Type u_2}
[TopologicalSpace L]
[TopologicalSpace X]
[Sup L]
[ContinuousSup L]
{f : X → L}
{g : X → L}
{s : Set X}
(hf : ContinuousOn f s)
(hg : ContinuousOn g s)
:
ContinuousOn (f ⊔ g) s
theorem
ContinuousOn.sup
{L : Type u_1}
{X : Type u_2}
[TopologicalSpace L]
[TopologicalSpace X]
[Sup L]
[ContinuousSup L]
{f : X → L}
{g : X → L}
{s : Set X}
(hf : ContinuousOn f s)
(hg : ContinuousOn g s)
:
ContinuousOn (fun (a : X) => f a ⊔ g a) s
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 (f ⊔ g)
theorem
ContinuousAt.inf'
{L : Type u_1}
{X : Type u_2}
[TopologicalSpace L]
[TopologicalSpace X]
[Inf L]
[ContinuousInf L]
{f : X → L}
{g : X → L}
{x : X}
(hf : ContinuousAt f x)
(hg : ContinuousAt g x)
:
ContinuousAt (f ⊓ g) x
theorem
ContinuousAt.inf
{L : Type u_1}
{X : Type u_2}
[TopologicalSpace L]
[TopologicalSpace X]
[Inf L]
[ContinuousInf L]
{f : X → L}
{g : X → L}
{x : X}
(hf : ContinuousAt f x)
(hg : ContinuousAt g x)
:
ContinuousAt (fun (a : X) => f a ⊓ g a) x
theorem
ContinuousWithinAt.inf'
{L : Type u_1}
{X : Type u_2}
[TopologicalSpace L]
[TopologicalSpace X]
[Inf L]
[ContinuousInf L]
{f : X → L}
{g : X → L}
{s : Set X}
{x : X}
(hf : ContinuousWithinAt f s x)
(hg : ContinuousWithinAt g s x)
:
ContinuousWithinAt (f ⊓ g) s x
theorem
ContinuousWithinAt.inf
{L : Type u_1}
{X : Type u_2}
[TopologicalSpace L]
[TopologicalSpace X]
[Inf L]
[ContinuousInf L]
{f : X → L}
{g : X → L}
{s : Set X}
{x : X}
(hf : ContinuousWithinAt f s x)
(hg : ContinuousWithinAt g s x)
:
ContinuousWithinAt (fun (a : X) => f a ⊓ g a) s x
theorem
ContinuousOn.inf'
{L : Type u_1}
{X : Type u_2}
[TopologicalSpace L]
[TopologicalSpace X]
[Inf L]
[ContinuousInf L]
{f : X → L}
{g : X → L}
{s : Set X}
(hf : ContinuousOn f s)
(hg : ContinuousOn g s)
:
ContinuousOn (f ⊓ g) s
theorem
ContinuousOn.inf
{L : Type u_1}
{X : Type u_2}
[TopologicalSpace L]
[TopologicalSpace X]
[Inf L]
[ContinuousInf L]
{f : X → L}
{g : X → L}
{s : Set X}
(hf : ContinuousOn f s)
(hg : ContinuousOn g s)
:
ContinuousOn (fun (a : X) => f a ⊓ g a) s
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 (f ⊓ g)
theorem
ContinuousAt.finset_sup'_apply
{L : Type u_1}
{X : Type u_2}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeSup L]
[ContinuousSup L]
{s : Finset ι}
{f : ι → X → L}
{x : X}
(hne : s.Nonempty)
(hs : ∀ i ∈ s, 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}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeSup L]
[ContinuousSup L]
{s : Finset ι}
{f : ι → X → L}
{x : X}
(hne : s.Nonempty)
(hs : ∀ i ∈ s, ContinuousAt (f i) x)
:
ContinuousAt (s.sup' hne f) x
theorem
ContinuousWithinAt.finset_sup'_apply
{L : Type u_1}
{X : Type u_2}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeSup L]
[ContinuousSup L]
{s : Finset ι}
{f : ι → X → L}
{t : Set X}
{x : X}
(hne : s.Nonempty)
(hs : ∀ i ∈ s, 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}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeSup L]
[ContinuousSup L]
{s : Finset ι}
{f : ι → X → L}
{t : Set X}
{x : X}
(hne : s.Nonempty)
(hs : ∀ i ∈ s, 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}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeSup L]
[ContinuousSup L]
{s : Finset ι}
{f : ι → X → L}
{t : Set X}
(hne : s.Nonempty)
(hs : ∀ i ∈ s, 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}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeSup L]
[ContinuousSup L]
{s : Finset ι}
{f : ι → X → L}
{t : Set X}
(hne : s.Nonempty)
(hs : ∀ i ∈ s, ContinuousOn (f i) t)
:
ContinuousOn (s.sup' hne f) t
theorem
Continuous.finset_sup'_apply
{L : Type u_1}
{X : Type u_2}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeSup L]
[ContinuousSup L]
{s : Finset ι}
{f : ι → X → L}
(hne : s.Nonempty)
(hs : ∀ i ∈ s, 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}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeSup L]
[ContinuousSup L]
{s : Finset ι}
{f : ι → X → L}
(hne : s.Nonempty)
(hs : ∀ i ∈ s, Continuous (f i))
:
Continuous (s.sup' hne f)
theorem
ContinuousAt.finset_sup_apply
{L : Type u_1}
{X : Type u_2}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeSup L]
[OrderBot L]
[ContinuousSup L]
{s : Finset ι}
{f : ι → X → L}
{x : X}
(hs : ∀ i ∈ s, 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}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeSup L]
[OrderBot L]
[ContinuousSup L]
{s : Finset ι}
{f : ι → X → L}
{x : X}
(hs : ∀ i ∈ s, ContinuousAt (f i) x)
:
ContinuousAt (s.sup f) x
theorem
ContinuousWithinAt.finset_sup_apply
{L : Type u_1}
{X : Type u_2}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeSup L]
[OrderBot L]
[ContinuousSup L]
{s : Finset ι}
{f : ι → X → L}
{t : Set X}
{x : X}
(hs : ∀ i ∈ s, 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}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeSup L]
[OrderBot L]
[ContinuousSup L]
{s : Finset ι}
{f : ι → X → L}
{t : Set X}
{x : X}
(hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x)
:
ContinuousWithinAt (s.sup f) t x
theorem
ContinuousOn.finset_sup_apply
{L : Type u_1}
{X : Type u_2}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeSup L]
[OrderBot L]
[ContinuousSup L]
{s : Finset ι}
{f : ι → X → L}
{t : Set X}
(hs : ∀ i ∈ s, 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}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeSup L]
[OrderBot L]
[ContinuousSup L]
{s : Finset ι}
{f : ι → X → L}
{t : Set X}
(hs : ∀ i ∈ s, ContinuousOn (f i) t)
:
ContinuousOn (s.sup f) t
theorem
Continuous.finset_sup_apply
{L : Type u_1}
{X : Type u_2}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeSup L]
[OrderBot L]
[ContinuousSup L]
{s : Finset ι}
{f : ι → X → L}
(hs : ∀ i ∈ s, 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}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeSup L]
[OrderBot L]
[ContinuousSup L]
{s : Finset ι}
{f : ι → X → L}
(hs : ∀ i ∈ s, Continuous (f i))
:
Continuous (s.sup f)
theorem
ContinuousAt.finset_inf'_apply
{L : Type u_1}
{X : Type u_2}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeInf L]
[ContinuousInf L]
{s : Finset ι}
{f : ι → X → L}
{x : X}
(hne : s.Nonempty)
(hs : ∀ i ∈ s, 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}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeInf L]
[ContinuousInf L]
{s : Finset ι}
{f : ι → X → L}
{x : X}
(hne : s.Nonempty)
(hs : ∀ i ∈ s, ContinuousAt (f i) x)
:
ContinuousAt (s.inf' hne f) x
theorem
ContinuousWithinAt.finset_inf'_apply
{L : Type u_1}
{X : Type u_2}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeInf L]
[ContinuousInf L]
{s : Finset ι}
{f : ι → X → L}
{t : Set X}
{x : X}
(hne : s.Nonempty)
(hs : ∀ i ∈ s, 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}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeInf L]
[ContinuousInf L]
{s : Finset ι}
{f : ι → X → L}
{t : Set X}
{x : X}
(hne : s.Nonempty)
(hs : ∀ i ∈ s, 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}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeInf L]
[ContinuousInf L]
{s : Finset ι}
{f : ι → X → L}
{t : Set X}
(hne : s.Nonempty)
(hs : ∀ i ∈ s, 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}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeInf L]
[ContinuousInf L]
{s : Finset ι}
{f : ι → X → L}
{t : Set X}
(hne : s.Nonempty)
(hs : ∀ i ∈ s, ContinuousOn (f i) t)
:
ContinuousOn (s.inf' hne f) t
theorem
Continuous.finset_inf'_apply
{L : Type u_1}
{X : Type u_2}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeInf L]
[ContinuousInf L]
{s : Finset ι}
{f : ι → X → L}
(hne : s.Nonempty)
(hs : ∀ i ∈ s, 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}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeInf L]
[ContinuousInf L]
{s : Finset ι}
{f : ι → X → L}
(hne : s.Nonempty)
(hs : ∀ i ∈ s, Continuous (f i))
:
Continuous (s.inf' hne f)
theorem
ContinuousAt.finset_inf_apply
{L : Type u_1}
{X : Type u_2}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeInf L]
[OrderTop L]
[ContinuousInf L]
{s : Finset ι}
{f : ι → X → L}
{x : X}
(hs : ∀ i ∈ s, 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}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeInf L]
[OrderTop L]
[ContinuousInf L]
{s : Finset ι}
{f : ι → X → L}
{x : X}
(hs : ∀ i ∈ s, ContinuousAt (f i) x)
:
ContinuousAt (s.inf f) x
theorem
ContinuousWithinAt.finset_inf_apply
{L : Type u_1}
{X : Type u_2}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeInf L]
[OrderTop L]
[ContinuousInf L]
{s : Finset ι}
{f : ι → X → L}
{t : Set X}
{x : X}
(hs : ∀ i ∈ s, 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}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeInf L]
[OrderTop L]
[ContinuousInf L]
{s : Finset ι}
{f : ι → X → L}
{t : Set X}
{x : X}
(hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x)
:
ContinuousWithinAt (s.inf f) t x
theorem
ContinuousOn.finset_inf_apply
{L : Type u_1}
{X : Type u_2}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeInf L]
[OrderTop L]
[ContinuousInf L]
{s : Finset ι}
{f : ι → X → L}
{t : Set X}
(hs : ∀ i ∈ s, 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}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeInf L]
[OrderTop L]
[ContinuousInf L]
{s : Finset ι}
{f : ι → X → L}
{t : Set X}
(hs : ∀ i ∈ s, ContinuousOn (f i) t)
:
ContinuousOn (s.inf f) t
theorem
Continuous.finset_inf_apply
{L : Type u_1}
{X : Type u_2}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeInf L]
[OrderTop L]
[ContinuousInf L]
{s : Finset ι}
{f : ι → X → L}
(hs : ∀ i ∈ s, 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}
[TopologicalSpace L]
[TopologicalSpace X]
{ι : Type u_3}
[SemilatticeInf L]
[OrderTop L]
[ContinuousInf L]
{s : Finset ι}
{f : ι → X → L}
(hs : ∀ i ∈ s, Continuous (f i))
:
Continuous (s.inf f)