English
The neighborhood of the infimum of two filters equals the infimum of their neighborhoods: 𝓝(l1 ⊓ l2) = 𝓝(l1) ⊓ 𝓝(l2).
Русский
Окрестности пересечения двух фильтров равны пересечению их окрестностей: 𝓝(l1 ⊓ l2) = 𝓝(l1) ⊓ 𝓝(l2).
LaTeX
$$$𝓝(l_1 \sqcap l_2) = 𝓝(l_1) \sqcap 𝓝(l_2).$$$
Lean4
@[simp]
protected theorem nhds_inf (l₁ l₂ : Filter α) : 𝓝 (l₁ ⊓ l₂) = 𝓝 l₁ ⊓ 𝓝 l₂ := by
simpa only [iInf_bool_eq] using Filter.nhds_iInf fun b => cond b l₁ l₂