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 _)