isClosedEmbedding_mk — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem isClosedEmbedding_mk : IsClosedEmbedding (@mk M) :=
  mkHomeomorph.isClosedEmbedding

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