finset_sup' — Mathlib

English

If s is a nonempty Finset and each f_i is Continuous, then the finite supremum s.sup' hne f is Continuous.

Русский

Если s непусто; каждая f_i непрерывна; то s.sup' hne f непрерывна.

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 (s.sup' hne f).$$$

Lean4

theorem finset_sup' (hne : s.Nonempty) (hs : ∀ i ∈ s, Continuous (f i)) : Continuous (s.sup' hne f) :=
  continuous_iff_continuousAt.2 fun _ ↦ ContinuousAt.finset_sup' _ fun i hi ↦ (hs i hi).continuousAt

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