English
Let L and X be topological spaces, ι a type, s a finite set of indices, and f : ι → X → L with each f_i continuous on X. Then the map a ↦ s.sup (f · a) is continuous on X.
Русский
Пусть L и X — топологические пространства, ι — тип, s — конечный набор индексов, f : ι → X → L, и каждый f_i непрерывен на X. Тогда функция a ↦ sup_{i ∈ s} f_i(a) непрерывна на 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_apply (hs : ∀ i ∈ s, Continuous (f i)) : Continuous (fun a ↦ s.sup (f · a)) :=
continuous_iff_continuousAt.2 fun _ ↦ ContinuousAt.finset_sup_apply fun i hi ↦ (hs i hi).continuousAt
