English
For a nonempty Finset s and a family f, if each f_i is ContinuousWithinAt (f i) t x for i ∈ s, then a ↦ s.sup' hne (f · a) is ContinuousWithinAt at x with respect to t.
Русский
Пусть s непусто и конечно; если для всех i ∈ s функция f_i непрерывна внутри t в x, то a ↦ sup'_{i∈s} f_i(a) непрерывна внутри 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 (\\lambda a => s.sup' hne (f · a)) t x.$$$
Lean4
theorem finset_sup'_apply (hne : s.Nonempty) (hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x) :
ContinuousWithinAt (fun a ↦ s.sup' hne (f · a)) t x :=
Tendsto.finset_sup'_nhds_apply hne hs
