partialSups — Mathlib

English

If each f_k is Continuous on α for k ≤ n, then a ↦ partialSups f n is Continuous on α.

Русский

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

LaTeX

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

Lean4

protected theorem partialSups (hf : ∀ k ≤ n, Continuous (f k)) : Continuous (partialSups f n) :=
  continuous_iff_continuousAt.2 fun _ ↦ ContinuousAt.partialSups fun k hk ↦ (hf k hk).continuousAt

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