partialSups — Mathlib

English

If all f_k are ContinuousOn on s, then the map a ↦ partialSups f n is ContinuousOn on s.

Русский

Если все f_k непрерывны на s, то 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 (partialSups f n) s.$$$

Lean4

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

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