English
Let s be a finite nonempty index set, and f_i: X → L continuous at x for each i ∈ s. Then the map a ↦ sup'_{i∈s} f_i(a) is continuous at x.
Русский
Пусть s конечное множество индексов, и для каждого i ∈ s функция f_i: X → L непрерывна в x; тогда a ↦ sup'_{i∈s} f_i(a) непрерывна в x.
LaTeX
$$$\\forall L X\\ [TopologicalSpace L]\\ [TopologicalSpace X]\\ {s : Finset ι},\\ {f : ι \\to X \\to L},\\ {x : X},\\ (s.Nonempty)\\to (\\forall i ∈ s, ContinuousAt (f i) x)\\Rightarrow\\ ContinuousAt (\\lambda a \\mapsto s.sup' H (f \\cdot a)) x.$$$
Lean4
theorem finset_sup'_apply (hne : s.Nonempty) (hs : ∀ i ∈ s, ContinuousAt (f i) x) :
ContinuousAt (fun a ↦ s.sup' hne (f · a)) x :=
Tendsto.finset_sup'_nhds_apply hne hs
