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)