English
For a family of filters f: 𝕴 → Filter α, the neighborhood of the infimum equals the infimum of the neighborhoods: 𝓝(⨅ i, f i) = ⨅ i, 𝓝(f i).
Русский
Окрестности инфимума: 𝓝(⨅ i, f(i)) = ⨅ i, 𝓝(f(i)).
LaTeX
$$@[simp]\nprotected theorem nhds_iInf (f : ι → Filter α) : 𝓝 (⨅ i, f i) = ⨅ i, 𝓝 (f i)$$
Lean4
@[simp]
protected theorem nhds_iInf (f : ι → Filter α) : 𝓝 (⨅ i, f i) = ⨅ i, 𝓝 (f i) :=
by
simp only [nhds_eq]
apply lift'_iInf_of_map_univ <;> simp