sup_nhds — Mathlib

English

If f,g: α → L converge to x,y, then the supremum of their images converges to the supremum of the limits.

Русский

Если функции f и g сходятся к x и y, то их точечный суп сходится к x ⊔ y.

LaTeX

$$$\\text{Tendsto} f\, l\\ (\\mathcal{N} x) \\land \\text{Tendsto} g\, l\\ (\\mathcal{N} y) \\Rightarrow \\text{Tendsto}(f \\sqcup g) l\\ (\\mathcal{N}(x \\sqcup y))$$$

Lean4

theorem sup_nhds [Max L] [ContinuousSup L] (hf : Tendsto f l (𝓝 x)) (hg : Tendsto g l (𝓝 y)) :
    Tendsto (fun i => f i ⊔ g i) l (𝓝 (x ⊔ y)) :=
  hf.sup_nhds' hg

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