English
Let s be a nonempty Finset and f_i: X → L. If each f_i is ContinuousOn (f i) t, then a ↦ s.sup' hne (f · a) is ContinuousOn t.
Русский
Пусть s непусто; если для каждого i ∈ s функция f_i непрерывна на t, то a ↦ sup'_{i∈s} f_i(a) непрерывна на t.
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, ContinuousOn (f i) t)\\Rightarrow ContinuousOn (\\lambda a \\mapsto s.sup' hne (f \\cdot a)) t.$$$
Lean4
theorem finset_sup'_apply (hne : s.Nonempty) (hs : ∀ i ∈ s, ContinuousOn (f i) t) :
ContinuousOn (fun a ↦ s.sup' hne (f · a)) t := fun x hx ↦
ContinuousWithinAt.finset_sup'_apply hne fun i hi ↦ hs i hi x hx
