English
Let L be a topological semilattice with a bottom element, X a topological space, t a subset of X, and s a finite index set. If each f_i : X → L is ContinuousOn t for all i ∈ s, then the function x ↦ sup_{i ∈ s} f_i(x) is ContinuousOn t.
Русский
Пусть L — топологическая полупорядованная множество с операцией обобщения (sup) и нулём, X — топологическое пространство, t ⊆ X, s — конечный набор индексов. Пусть f_i : X → L для всех i ∈ s и каждый f_i непрерывен на t. Тогда функция x ↦ sup_{i ∈ s} f_i(x) непрерывна на t.
LaTeX
$$$\left(\forall i \in s,\ \text{ContinuousOn}(f_i, t)\right) \Rightarrow \text{ContinuousOn}\left(x \mapsto \sup_{i \in s} f_i(x),\ t\right).$$$
Lean4
theorem finset_sup (hs : ∀ i ∈ s, ContinuousOn (f i) t) : ContinuousOn (s.sup f) t := fun x hx ↦
ContinuousWithinAt.finset_sup fun i hi ↦ hs i hi x hx
