partialSups_apply — Mathlib

English

If each f_k is continuous at x, then the map a ↦ partialSups (f · a) n is continuous at x (in the sense of evaluation at that point).

Русский

Если все f_k непрерывны в точке x, то отображение a ↦ частичная верхняя сумма ∨_{k≤n} f_k(a) непрерывно в точке x.

LaTeX

$$$\\forall L\\ [SemilatticeSup L]\\ [TopologicalSpace L]\\ [ContinuousSup L]\\ [TopologicalSpace X]\\\\forall f:\\mathbb{N}\\to X\\to L,\\forall n,\\forall x,\\Big(\\forall k≤n,\\ ContinuousAt (f k) x\\Big)\\Rightarrow\\ ContinuousAt (a\\mapsto partialSups (f\\cdot a)\\ n) x.$$$

Lean4

protected theorem partialSups_apply (hf : ∀ k ≤ n, ContinuousAt (f k) x) :
    ContinuousAt (fun a ↦ partialSups (f · a) n) x :=
  Tendsto.partialSups_apply hf

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