English
If hne is a nonempty finite index set and each f_i is ContinuousAt (f i) at x, then the map a ↦ s.sup' hne (f · a) is ContinuousAt at x.
Русский
Если s непусто и конечна, и для каждого i ∈ s функция f_i имеет ContinuousAt в x, то a ↦ sup'_{i∈s} f_i(a) непрерывна в x.
LaTeX
$$$\\forall L X\\ [TopologicalSpace L]\\ [TopologicalSpace X]\\ {ι : Type*}\\ {s : Finset ι} {f : ι \\to X \\to L} {x : X},\\ (s.Nonempty)\\to (\\forall i ∈ s, ContinuousAt (f i) x)\\Rightarrow ContinuousAt (\\lambda a => s.sup' hne (f · a)) x.$$$
Lean4
theorem finset_sup' (hne : s.Nonempty) (hs : ∀ i ∈ s, ContinuousAt (f i) x) : ContinuousAt (s.sup' hne f) x := by
simpa only [← Finset.sup'_apply] using finset_sup'_apply hne hs
