nhds_principal — Mathlib

English

The neighborhoods of the principal filter 𝓟 S are exactly the principal filter generated by the downward-closure of 𝓟 S: 𝓝(𝓟 S) = 𝓟(Iic(𝓟 S)).

Русский

Окрестности принципиального фильтра 𝓟 S равны принципиальному фильтру, порождённому Iic(𝓟 S).

LaTeX

$$$𝓝(𝓟 S) = 𝓟\left( Iic\big( 𝓟 S \big) \right).$$$

Lean4

@[simp]
theorem nhds_principal (s : Set α) : 𝓝 (𝓟 s) = 𝓟 (Iic (𝓟 s)) :=
  (hasBasis_principal s).nhds.eq_of_same_basis (hasBasis_principal _)

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