inf_nhds' — Mathlib

English

If f,g: α → L converge to x,y respectively, 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 \\sqcap g) l (\\mathcal{N}(x \\sqcap y))$$$

Lean4

theorem inf_nhds' [Min L] [ContinuousInf L] (hf : Tendsto f l (𝓝 x)) (hg : Tendsto g l (𝓝 y)) :
    Tendsto (f ⊓ g) l (𝓝 (x ⊓ y)) :=
  (continuous_inf.tendsto _).comp (hf.prodMk_nhds hg)

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