map_proj_nhds — Mathlib

English

For any x, the projection map sends the neighborhood filter at x to the neighborhood filter at proj(x).

Русский

Для любого x отображение proj отправляет фильтр окрестностей x в фильтр окрестностей proj(x).

LaTeX

$$$ map\ proj\ (nhds\ x) = nhds\ (proj\ x) $$$

Lean4

theorem map_proj_nhds (ex : x ∈ e.source) : map proj (𝓝 x) = 𝓝 (proj x) := by
  rw [← e.coe_fst ex, ← map_congr (e.coe_fst_eventuallyEq_proj ex), ← map_map, ← e.coe_coe, e.map_nhds_eq ex,
    map_fst_nhds]

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