finset_sup — Mathlib

English

If hne is nonempty and each f_i is ContinuousAt x, then the map a ↦ s.sup' hne (f · a) is ContinuousAt x.

Русский

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

LaTeX

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

Lean4

theorem finset_sup (hs : ∀ i ∈ s, ContinuousAt (f i) x) : ContinuousAt (s.sup f) x := by
  simpa only [← Finset.sup_apply] using finset_sup_apply hs

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