finset_sup — Mathlib

English

If every f_i is ContinuousWithinAt (f i) t x for i ∈ s, then s.sup f is ContinuousWithinAt t x.

Русский

Если все f_i непрерывны внутри t в x, то их конечный суп через f непрерывен внутри t в x.

LaTeX

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

Lean4

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

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