English
If each f_k is continuous within a set s at x for k ≤ n, then the map a ↦ partialSups (f · a) n is ContinuousWithinAt at x relative to s.
Русский
Если для всех k ≤ n функция f_k непрерывна внутри множества s в точке x, тогда a ↦ ∨_{k≤n} f_k(a) непрерывна внутри s в x.
LaTeX
$$$\\forall L\\ [SemilatticeSup L]\\ [TopologicalSpace L]\\ [ContinuousSup L]\\ \\forall X\\ [TopologicalSpace X],\\forall f:\\mathbb{N}\\to X\\to L,\\forall n,\\forall s:\\ Set X,\\Big(\\forall k≤n,\\ ContinuousWithinAt (f k) s x\\Big)\\Rightarrow\\ ContinuousWithinAt (a\\mapsto partialSups (f\\cdot a)\\ n) s x.$$$
Lean4
protected theorem partialSups_apply (hf : ∀ k ≤ n, ContinuousWithinAt (f k) s x) :
ContinuousWithinAt (fun a ↦ partialSups (f · a) n) s x :=
Tendsto.partialSups_apply hf
