English
For any point x in the total space, the image of the neighborhood filter under the projection equals the neighborhood filter at the projection of x.
Русский
Для любой точки x в общем пространстве образ фильтра окрестностей под проекцией совпадает с окрестностями базовой точки x.proj.
LaTeX
$$\( \operatorname{map}(\pi F E)(\mathcal{N}x)=\mathcal{N}(x.proj) \)$$
Lean4
theorem map_proj_nhds (x : TotalSpace F E) : map (π F E) (𝓝 x) = 𝓝 x.proj :=
(trivializationAt F E x.proj).map_proj_nhds <|
(trivializationAt F E x.proj).mem_source.2 <| mem_baseSet_trivializationAt F E x.proj