English
For a finite nonempty set s, the map a ↦ s.sup' hne (f · a) tends to s.sup' hne g if for every i ∈ s, Tendsto (f i) l (nhds (g i)).
Русский
Для непустого конечного множества s отображение a ↦ s.sup' hne (f · a) сходится к s.sup' hne g, если для каждого i ∈ s выполнено Tendsto (f i) l (nhds (g i)).
LaTeX
$$$\\text{Nonempty}(s) \\Rightarrow (\\forall i \\in s, \\text{Tendsto}(f_i) l (\\mathcal{N}(g_i))) \\Rightarrow \\text{Tendsto}(a \\mapsto s.\\mathrm{sup}'\\ hne (f \\!\\cdot\\ a)) l (\\mathcal{N}(s.\\mathrm{sup}'\\ hne g))$$$
Lean4
theorem finset_sup'_nhds_apply [SemilatticeSup L] [ContinuousSup L] (hne : s.Nonempty)
(hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) : Tendsto (fun a ↦ s.sup' hne (f · a)) l (𝓝 (s.sup' hne g)) := by
simpa only [← Finset.sup'_apply] using finset_sup'_nhds hne hs
