nhds_iInf — Mathlib

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

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