English
If each f_k is ContinuousWithinAt (f_k) s x for k ≤ n, then PartialSups f n is ContinuousWithinAt s x.
Русский
Если для каждого k ≤ n функция f_k непрерывна внутри s в x, то ∨_{k≤n} f_k непрерывна внутри 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 (partialSups f n) s x.$$$
Lean4
protected theorem partialSups (hf : ∀ k ≤ n, ContinuousWithinAt (f k) s x) : ContinuousWithinAt (partialSups f n) s x :=
by simpa only [← Pi.partialSups_apply] using ContinuousWithinAt.partialSups_apply hf
