nhds_inl

Mathlib.Topology.Instances.TrivSqZeroExt

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

English

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

Русский

При [Zero M] окрестности от inl x равны окрестностям x в R и нулевой окрестности в M.

LaTeX

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

Lean4

theorem nhds_inl [Zero M] (x : R) : 𝓝 (inl x : tsze R M) = 𝓝 x ×ˢ 𝓝 0 :=
  nhds_def _

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

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

Разделы

Аффилиация

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