nhds_inr

Mathlib.Topology.Instances.TrivSqZeroExt

URI: https://scilib.ai/kg/mathlib#TrivSqZeroExt.nhds_inr

English

For [Zero R], nhds(inr m) = nhds 0 × nhds m for m ∈ M.

Русский

При [Zero R] окрестности от inr m равны нулевой окрестности в R и окрестности m в M.

LaTeX

$$$\\mathcal{N}(\\mathrm{inr}(m))=\\mathcal{N}_{R}(0) \\times \\mathcal{N}_{M}(m).$$$

Lean4

theorem nhds_inr [Zero R] (m : M) : 𝓝 (inr m : tsze R M) = 𝓝 0 ×ˢ 𝓝 m :=
  nhds_def _

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

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

Разделы

Аффилиация

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