partialSups — Mathlib

English

If each f_k is continuous at x for k ≤ n, then the map a ↦ partialSups f n is continuous at x.

Русский

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

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,\\ ContinuousAt (f k) x\\Big)\\Rightarrow\\ ContinuousAt (partialSups f n) x.$$$

Lean4

protected theorem partialSups (hf : ∀ k ≤ n, ContinuousAt (f k) x) : ContinuousAt (partialSups f n) x := by
  simpa only [← Pi.partialSups_apply] using ContinuousAt.partialSups_apply hf

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