instT4Space

Mathlib.Topology.Algebra.Constructions.DomMulAct

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

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
instance instT4Space [T4Space M] : T4Space Mᵈᵐᵃ :=
  mkHomeomorph.t4Space

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

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

Разделы

Аффилиация

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