English
Let s be a finite index set. If each f_i tends to g_i, then the finite supremum of the f_i tends to the finite supremum of the g_i.
Русский
Пусть s — конечное множество индексов. Если для каждого i ∈ s выполняется Tendsto(f_i) к g_i, то sup_{i∈s} f_i сходится к sup_{i∈s} g_i.
LaTeX
$$$\\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] [OrderBot L] [ContinuousSup L] (hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) :
Tendsto (s.sup f) l (𝓝 (s.sup g)) :=
by
rcases s.eq_empty_or_nonempty with rfl | hne
· simpa using tendsto_const_nhds
· simp only [← sup'_eq_sup hne]
exact finset_sup'_nhds hne hs
