English
For a finite set s and functions f_i: α → L, if Tendsto (f_i) l to nhds (g_i) for all i, then a certain function a ↦ s.sup' hne (f i) tends to s.sup' hne g.
Русский
Для конечного множества s и функций f_i: α → L, если Tendsto(f_i) к g_i для всех i, то a ↦ s.sup' hne (f · a) сходится к s.sup' hne g.
LaTeX
$$$\\text{Nonempty}(s) \\Rightarrow (\\forall i, i\\in s \\rightarrow \\text{Tendsto}(f_i) l (\\mathcal{N}(g_i))) \\Rightarrow \\text{Tendsto}(a \\mapsto s.\\mathrm{sup}' hne (f i)) l (\\mathcal{N}(s.\\mathrm{sup}' hne g))$$$
Lean4
theorem finset_sup_nhds_apply [SemilatticeSup L] [OrderBot L] [ContinuousSup L]
(hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) : Tendsto (fun a ↦ s.sup (f · a)) l (𝓝 (s.sup g)) := by
simpa only [← Finset.sup_apply] using finset_sup_nhds hs
