finset_sup_apply — Mathlib

English

For a nonempty Finset s and ContinuousWithinAt (f i) t x, the map a ↦ s.sup (f · a) is ContinuousWithinAt t x.

Русский

Если s непусто и каждый f_i непрерывно внутри t в x, то a ↦ sup_{i∈s} f_i(a) внутри t в x непрерывна.

LaTeX

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

Lean4

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

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