nhds_inr — Mathlib

English

For any y in Y, the neighborhood of the right-injection of y into the disjoint sum X ⊕ Y is obtained by pushing forward the neighborhood of y along the injection.

Русский

Пусть y принадлежит Y. Окрестности точки inr(y) в сумме X ⊕ Y совпадают с образами окрестностей y под линейной вложением inr.

LaTeX

$$$$\\mathcal{N}(\\mathrm{inr}(y)) = \\mathrm{map}(\\mathrm{inr})(\\mathcal{N}(y)).$$$$

Lean4

theorem nhds_inr (y : Y) : 𝓝 (inr y : X ⊕ Y) = map inr (𝓝 y) :=
  (IsOpenEmbedding.inr.map_nhds_eq _).symm

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