English
Let s be a nonempty Finset of indices and f_i: X → L. If each f_i is ContinuousOn on t, then the function a ↦ s.sup' hne f is ContinuousOn t.
Русский
Пусть s непусто; если каждый f_i непрерывна на t, то сумма через sup' непрерывна на t.
LaTeX
$$$\\forall L X\\ [TopologicalSpace L]\\ [TopologicalSpace X]\\ {ι : Type*}\\ {s : Finset ι} {f : ι \\to X \\to L} {t : Set X} {x : X},\\ (s.Nonempty)\\to (\\forall i ∈ s, ContinuousOn (f i) t)\\Rightarrow ContinuousOn (\\lambda a \\mapsto s.sup' hne (f \\cdot a)) t.$$$
Lean4
theorem finset_sup' (hne : s.Nonempty) (hs : ∀ i ∈ s, ContinuousOn (f i) t) : ContinuousOn (s.sup' hne f) t :=
fun x hx ↦ ContinuousWithinAt.finset_sup' hne fun i hi ↦ hs i hi x hx
