English
Let s be a nonempty finite set of indices. If each f_i converges to g_i, then the finite supremum over s of the f_i converges to the finite supremum over s of the g_i.
Русский
Пусть s — непустое конечное множество индексов. Если каждый f_i сходится к g_i, то их конечный верхний предел сходится к верхнему пределу этих g_i.
LaTeX
$$$\\text{Nonempty}(s) \\Rightarrow (\\forall i \\in s, \\text{Tendsto}(f_i) l (\\mathcal{N}(g_i))) \\Rightarrow \\text{Tendsto}(s.\\mathrm{sup}\\ f) l (\\mathcal{N}(s.\\mathrm{sup}\\ g))$$$
Lean4
theorem finset_sup'_nhds [SemilatticeSup L] [ContinuousSup L] (hne : s.Nonempty)
(hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) : Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g)) := by
induction hne using Finset.Nonempty.cons_induction with
| singleton => simpa using hs
| cons a s ha hne ihs =>
rw [forall_mem_cons] at hs
simp only [sup'_cons, hne]
exact hs.1.sup_nhds (ihs hs.2)
