English
The neighborhood filter at l is the lift of the principal filter along Iic ∘ 𝓟.
Русский
Фильтр окрестностей l — подъём главного фильтра по Iic ∘ 𝓟.
LaTeX
$$$$\mathcal{N}(l)=l.lift'(Iic\circ 𝓟).$$$$
Lean4
theorem nhds_eq (l : Filter α) : 𝓝 l = l.lift' (Iic ∘ 𝓟) :=
nhds_generateFrom.trans <| by
simp only [mem_setOf_eq, @and_comm (l ∈ _), iInf_and, iInf_range, Filter.lift', Filter.lift, (· ∘ ·), mem_Iic,
le_principal_iff]