English
Let L be a semilattice with sup, and l a filter. If f, g are sequences of functions with f_k → g_k along l for all k ≤ n, then the partial supremum up to n satisfies Tendsto(f) → Tendsto(g) at level n; i.e., the map a ↦ ∨_{k≤n} f_k(a) tends to ∨_{k≤n} g_k as a varies along l.
Русский
Пусть L — полугодо-множество с верхней суммой, l — фильтр. Если последовательности функций f_k и g_k удовлетворяют f_k → g_k по l для всех k ≤ n, тогда частичная верхняя сумма до n сохраняет предел: ∨_{k≤n} f_k(a) → ∨_{k≤n} g_k(a).
LaTeX
$$$\\forall L\\ [SemilatticeSup L]\\ [TopologicalSpace L]\\ [ContinuousSup L],\\forall \\alpha\\, l\\ (l\\text{ фільтр на }\\alpha),\\forall f,g:\\mathbb{N}\\to\\alpha\\to L,\\forall n,\\Big(\\forall k\\le n,\\ Tendsto (f_k)\\ l\\ (\\mathcal{nhds}(g_k))\\Big)\\Rightarrow\\ Tendsto(\\partialSups f\\ n)\\ l\\ (\\mathcal{nhds}(\\partialSups g\\ n)).$$$
Lean4
protected theorem partialSups (hf : ∀ k ≤ n, Tendsto (f k) l (𝓝 (g k))) :
Tendsto (partialSups f n) l (𝓝 (partialSups g n)) :=
by
simp only [partialSups_eq_sup'_range]
refine finset_sup'_nhds _ ?_
simpa [Nat.lt_succ_iff]
