mkHomeomorph — Mathlib

English

There is a homeomorphism between M and Mᵈᵐᵃ given by mk, i.e., mkHomeomorph is a homeomorphism.

Русский

Существует гомеоморфизм между M и Mᵈᵐᵃ, заданный отображением mk; mkHomeomorph — гомеоморфизм.

LaTeX

$$$DomMulAct.mkHomeomorph : M \simeq_t M^{\mathrm{d}\mathrm{m}\mathrm{a}}$$$

Lean4

/-- `DomMulAct.mk` as a homeomorphism. -/
@[to_additive (attr := simps toEquiv) /-- `DomAddAct.mk` as a homeomorphism. -/
    ]
def mkHomeomorph : M ≃ₜ Mᵈᵐᵃ where
  toEquiv := mk
  continuous_toFun := by dsimp; fun_prop
  continuous_invFun := by dsimp; fun_prop

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