partialSups_apply — Mathlib

English

If for all k ≤ n, f_k is Continuous on α, then a ↦ partialSups (f · a) n is Continuous on α.

Русский

Если для всех k ≤ n функция f_k непрерывна на области, то 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\\cdot a)\\ n).$$$

Lean4

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

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