nhds_inf — Mathlib

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₂

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