isOpenEmbedding_mk — Mathlib

English

The canonical map mk is an open embedding; it is an open topological embedding of M into Mᵈᵐᵃ.

Русский

Каноническое отображение mk является открытым вложением; оно открытое топологическое вложение M в Mᵈᵐᵃ.

LaTeX

$$$ \\operatorname{IsOpenEmbedding}(\\operatorname{toFun}(\\mathrm{mk}))$$$

Lean4

@[to_additive]
theorem isOpenEmbedding_mk : IsOpenEmbedding (@mk M) :=
  mkHomeomorph.isOpenEmbedding

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