instCompletelyNormalSpace — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
instance instCompletelyNormalSpace [CompletelyNormalSpace M] : CompletelyNormalSpace Mᵈᵐᵃ :=
  isEmbedding_mk_symm.completelyNormalSpace

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