instR0Space

Mathlib.Topology.Algebra.Constructions.DomMulAct

URI: https://scilib.ai/kg/mathlib#DomMulAct.instR0Space

English

If M is R0, then Mᵈᵐᵃ is R0.

Русский

Если M — пространство R0, то Mᵈᵐᵃ также R0.

LaTeX

$$$ [R0Space\\ M] \\, \\Rightarrow \\, R0Space\\ M^{\\mathrm{DM}}$$

Lean4

@[to_additive]
instance instR0Space [R0Space M] : R0Space Mᵈᵐᵃ :=
  isEmbedding_mk_symm.r0Space

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

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

Разделы

Аффилиация

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