map_proj_nhds — Mathlib

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

Похожие утверждения