English
Let s be a nonempty Finset and f_i: X → L. If for all i ∈ s, f_i is ContinuousWithinAt (f i) t x, then the function a ↦ s.sup' hne f is ContinuousWithinAt t x.
Русский
Пусть s непусто и конечно; если для каждого i ∈ s функция f_i непрерывна внутри t в x, то сумма через sup' непрерывна внутри t в x.
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, ContinuousWithinAt (f i) t x)\\Rightarrow ContinuousWithinAt (s.sup' hne f) t x.$$$
Lean4
theorem finset_sup' (hne : s.Nonempty) (hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x) :
ContinuousWithinAt (s.sup' hne f) t x := by simpa only [← Finset.sup'_apply] using finset_sup'_apply hne hs
