sup_nhds' — Mathlib

English

If f,g: α → L tend to x,y respectively, then f ⊔ g tends to x ⊔ y.

Русский

Если f и g сходятся к x и y соответственно, то f ⊔ g сходится к x ⊔ y.

LaTeX

$$$\\text{Tendsto}(f,l,\\mathcal{N}(x)) \\rightarrow \\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 (f ⊔ g) l (𝓝 (x ⊔ y)) :=
  (continuous_sup.tendsto _).comp (hf.prodMk_nhds hg)

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