English
If a nonempty Finset s and a family f: ι → X → L are all Continuous (not just ContinuousOn) at every i, then the function a ↦ s.sup' hne (f · a) is Continuous.
Русский
Если все f_i непрерывны, то a ↦ sup'_{i∈s} f_i(a) непрерывна.
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, Continuous (f i))\\Rightarrow Continuous (\\lambda a \\mapsto s.sup' hne (f \\cdot a)).$$$
Lean4
theorem finset_sup'_apply (hne : s.Nonempty) (hs : ∀ i ∈ s, Continuous (f i)) :
Continuous (fun a ↦ s.sup' hne (f · a)) :=
continuous_iff_continuousAt.2 fun _ ↦ ContinuousAt.finset_sup'_apply _ fun i hi ↦ (hs i hi).continuousAt
