instRegularSpace

Mathlib.Topology.Algebra.Constructions.DomMulAct

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

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
instance instRegularSpace [RegularSpace M] : RegularSpace Mᵈᵐᵃ :=
  isEmbedding_mk_symm.regularSpace

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

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

Разделы

Аффилиация

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