English
The image of the restricted neighborhood filter under f is the infimum of principal filters generated by the images of open neighborhoods intersected with s: map f (𝓝[s] a) = ⨅ t open with a ∈ t of 𝓟(f''(t ∩ s)).
Русский
Образ фильтра окрестностей в пределах s под отображением f равен наименьшему фильтру-подчинению, порождённому множествами f''(t ∩ s) для открытых t, содержащих a.
LaTeX
$$$$\\\\mathrm{map}_f(\\\\mathcal{N}_s(a)) = \\\\bigwedge_{t: IsOpen, a ∈ t} \\\\mathcal{P}(f''(t \\\\cap s)).$$$$
Lean4
theorem map_nhdsWithin (f : α → β) (a : α) (s : Set α) :
map f (𝓝[s] a) = ⨅ t ∈ {t : Set α | a ∈ t ∧ IsOpen t}, 𝓟 (f '' (t ∩ s)) :=
((nhdsWithin_basis_open a s).map f).eq_biInf
