Continuity of partialSups #
In this file we prove that partialSups of a sequence of continuous functions is continuous
as well as versions for Filter.Tendsto, ContinuousAt, ContinuousWithinAt, and ContinuousOn.
theorem
Filter.Tendsto.partialSups
{L : Type u_1}
[SemilatticeSup L]
[TopologicalSpace L]
[ContinuousSup L]
{α : Type u_2}
{l : Filter α}
{f : ℕ → α → L}
{g : ℕ → L}
{n : ℕ}
(hf : ∀ k ≤ n, Filter.Tendsto (f k) l (nhds (g k)))
:
Filter.Tendsto ((partialSups f) n) l (nhds ((partialSups g) n))
theorem
Filter.Tendsto.partialSups_apply
{L : Type u_1}
[SemilatticeSup L]
[TopologicalSpace L]
[ContinuousSup L]
{α : Type u_2}
{l : Filter α}
{f : ℕ → α → L}
{g : ℕ → L}
{n : ℕ}
(hf : ∀ k ≤ n, Filter.Tendsto (f k) l (nhds (g k)))
:
Filter.Tendsto (fun (a : α) => (partialSups fun (x : ℕ) => f x a) n) l (nhds ((partialSups g) n))
theorem
ContinuousAt.partialSups_apply
{L : Type u_1}
[SemilatticeSup L]
[TopologicalSpace L]
[ContinuousSup L]
{X : Type u_2}
[TopologicalSpace X]
{f : ℕ → X → L}
{n : ℕ}
{x : X}
(hf : ∀ k ≤ n, ContinuousAt (f k) x)
:
ContinuousAt (fun (a : X) => (partialSups fun (x : ℕ) => f x a) n) x
theorem
ContinuousAt.partialSups
{L : Type u_1}
[SemilatticeSup L]
[TopologicalSpace L]
[ContinuousSup L]
{X : Type u_2}
[TopologicalSpace X]
{f : ℕ → X → L}
{n : ℕ}
{x : X}
(hf : ∀ k ≤ n, ContinuousAt (f k) x)
:
ContinuousAt ((partialSups f) n) x
theorem
ContinuousWithinAt.partialSups_apply
{L : Type u_1}
[SemilatticeSup L]
[TopologicalSpace L]
[ContinuousSup L]
{X : Type u_2}
[TopologicalSpace X]
{f : ℕ → X → L}
{n : ℕ}
{s : Set X}
{x : X}
(hf : ∀ k ≤ n, ContinuousWithinAt (f k) s x)
:
ContinuousWithinAt (fun (a : X) => (partialSups fun (x : ℕ) => f x a) n) s x
theorem
ContinuousWithinAt.partialSups
{L : Type u_1}
[SemilatticeSup L]
[TopologicalSpace L]
[ContinuousSup L]
{X : Type u_2}
[TopologicalSpace X]
{f : ℕ → X → L}
{n : ℕ}
{s : Set X}
{x : X}
(hf : ∀ k ≤ n, ContinuousWithinAt (f k) s x)
:
ContinuousWithinAt ((partialSups f) n) s x
theorem
ContinuousOn.partialSups_apply
{L : Type u_1}
[SemilatticeSup L]
[TopologicalSpace L]
[ContinuousSup L]
{X : Type u_2}
[TopologicalSpace X]
{f : ℕ → X → L}
{n : ℕ}
{s : Set X}
(hf : ∀ k ≤ n, ContinuousOn (f k) s)
:
ContinuousOn (fun (a : X) => (partialSups fun (x : ℕ) => f x a) n) s
theorem
ContinuousOn.partialSups
{L : Type u_1}
[SemilatticeSup L]
[TopologicalSpace L]
[ContinuousSup L]
{X : Type u_2}
[TopologicalSpace X]
{f : ℕ → X → L}
{n : ℕ}
{s : Set X}
(hf : ∀ k ≤ n, ContinuousOn (f k) s)
:
ContinuousOn ((partialSups f) n) s
theorem
Continuous.partialSups_apply
{L : Type u_1}
[SemilatticeSup L]
[TopologicalSpace L]
[ContinuousSup L]
{X : Type u_2}
[TopologicalSpace X]
{f : ℕ → X → L}
{n : ℕ}
(hf : ∀ k ≤ n, Continuous (f k))
:
Continuous fun (a : X) => (partialSups fun (x : ℕ) => f x a) n
theorem
Continuous.partialSups
{L : Type u_1}
[SemilatticeSup L]
[TopologicalSpace L]
[ContinuousSup L]
{X : Type u_2}
[TopologicalSpace X]
{f : ℕ → X → L}
{n : ℕ}
(hf : ∀ k ≤ n, Continuous (f k))
:
Continuous ((partialSups f) n)