English
Let L be a semilattice with topological structure and ContinuousSup. If for all k ≤ n we have Tendsto f_k l (nhds g_k), then the map a ↦ partialSups (f · a) n tends to partialSups g n along l.
Русский
Пусть L имеет верхнюю операцию и топологическую структуру; если для всех k ≤ n выполнено Tendsto f_k l (nhds g_k), тогда отображение a ↦ ∨_{k≤n} f_k(a) сходится к ∨_{k≤n} g_k.
LaTeX
$$$\\forall L\\ [SemilatticeSup L]\\ [TopologicalSpace L]\\ [ContinuousSup L]\\ \\forall \\alpha\\ \\forall l\\ \\forall f,g:\\mathbb{N}\\to\\alpha\\to L,\\forall n,\\Big(\\forall k≤n,\\ Tendsto (f k) l (nhds (g k))\\Big)\\Rightarrow\\ Tendsto (a\\mapsto partialSups (f\\cdot a)\\ n)\\ l\\ (nhds (partialSups g\\ n)).$$$
Lean4
protected theorem partialSups_apply (hf : ∀ k ≤ n, Tendsto (f k) l (𝓝 (g k))) :
Tendsto (fun a ↦ partialSups (f · a) n) l (𝓝 (partialSups g n)) := by
simpa only [← Pi.partialSups_apply] using Tendsto.partialSups hf
