isQuotientMap_mk — Mathlib

English

The canonical map mk is a quotient map; it induces the quotient topology from Mᵈᵐᵃ to M.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem isQuotientMap_mk : IsQuotientMap (@mk M) :=
  mkHomeomorph.isQuotientMap

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