finset_sup_apply — Mathlib

English

If f_i are continuous functions, then the function a ↦ s.sup' hne (f · a) is continuous.

Русский

Если функции f_i непрерывны, то a ↦ sup'_{i∈s} f_i(a) непрерывна.

LaTeX

$$$\\forall L X\\ [TopologicalSpace L]\\ [TopologicalSpace X]\\ {s : Finset ι}\\ {f : ι \\to X \\to L},\\ (s.Nonempty)\\to (\\forall i ∈ s, Continuous (f i))\\Rightarrow Continuous (\\lambda a => s.sup' hne (f \\cdot a)).$$$

Lean4

theorem finset_sup_apply (hs : ∀ i ∈ s, ContinuousAt (f i) x) : ContinuousAt (fun a ↦ s.sup (f · a)) x :=
  Tendsto.finset_sup_nhds_apply hs

Похожие утверждения