nhds_inl

Mathlib.Topology.Constructions.SumProd

URI: https://scilib.ai/kg/mathlib#nhds_inl

English

For x ∈ X, 𝓝(inl x) = map inl (𝓝 x).

Русский

Для x ∈ X: 𝓝( inl x ) = map inl ( 𝓝 x ).

LaTeX

$$$\\nhds(\\\\mathrm{inl}(x)) = (\\\\mathrm{map}\\\\, \\mathrm{inl})(\\nhds x)$$$

Lean4

theorem nhds_inl (x : X) : 𝓝 (inl x : X ⊕ Y) = map inl (𝓝 x) :=
  (IsOpenEmbedding.inl.map_nhds_eq _).symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru