English
The image filter of a neighborhood under a function is the infimum over images of open neighborhoods.
Русский
Образ фильтра окрестностей под функцией равен инфимууму образов открытых окрестностей.
LaTeX
$$$\\text{map}_f(\\mathcal N(x)) = \\bigwedge_{s\\ni x,\\ IsOpen(s)} \\mathcal P(f''s)$$$
Lean4
theorem map_nhds {f : X → α} : map f (𝓝 x) = ⨅ s ∈ {s : Set X | x ∈ s ∧ IsOpen s}, 𝓟 (f '' s) :=
((nhds_basis_opens x).map f).eq_biInf