inf_nhds — Mathlib

English

If f,g: α → L converge to x,y, then f ⊓ g converges to x ⊓ y.

Русский

Если f и g сходятся к x и y, тогда f ⊓ g сходится к x ⊓ y.

LaTeX

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

Lean4

theorem inf_nhds [Min L] [ContinuousInf L] (hf : Tendsto f l (𝓝 x)) (hg : Tendsto g l (𝓝 y)) :
    Tendsto (fun i => f i ⊓ g i) l (𝓝 (x ⊓ y)) :=
  hf.inf_nhds' hg

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