partialSups_apply — Mathlib

English

If f_k are ContinuousOn on s for all k ≤ n, then a ↦ partialSups (f · a) n is ContinuousOn on s.

Русский

Если f_k непрерывны на s для всех k ≤ n, то a ↦ ∨_{k≤n} f_k(a) непрерывна на s.

LaTeX

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

Lean4

protected theorem partialSups_apply (hf : ∀ k ≤ n, ContinuousOn (f k) s) :
    ContinuousOn (fun a ↦ partialSups (f · a) n) s := fun x hx ↦
  ContinuousWithinAt.partialSups_apply fun k hk ↦ hf k hk x hx

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