English
Let L be a topological semilattice with bottom, X a topological space, s a finite index set, f : ι → X → L. If every f_i is continuous (on all of X), then the function x ↦ sup_{i ∈ s} f_i(x) is continuous on X.
Русский
Пусть L — топологическая полупорядоченность с операцией верхнего объединения и нулём, X — топологическое пространство. Пусть s — конечный набор индексов, f_i : X → L. Если каждый f_i непрерывен на всем X, то x ↦ sup_{i ∈ s} f_i(x) непрерывна на X.
LaTeX
$$$\left(\forall i \in s,\ \text{Continuous}(f_i)\right) \Rightarrow \text{Continuous}\left(x \mapsto \sup_{i \in s} f_i(x)\right).$$$
Lean4
theorem finset_sup (hs : ∀ i ∈ s, Continuous (f i)) : Continuous (s.sup f) :=
continuous_iff_continuousAt.2 fun _ ↦ ContinuousAt.finset_sup fun i hi ↦ (hs i hi).continuousAt
