instEquivLike — Mathlib

English

A diffeomorphism h is continuous when viewed as an equivalence between manifolds.

Русский

Диффеоморфизм как отображение между многообразиями непрерывен.

LaTeX

$$$$ h \text{ continuous on the underlying spaces.} $$$$

Lean4

instance : EquivLike (M ≃ₘ^n⟮I, I'⟯ M') M M' where
  coe Φ := Φ.toEquiv
  inv Φ := Φ.toEquiv.symm
  left_inv Φ := Φ.left_inv
  right_inv Φ := Φ.right_inv
  coe_injective' _ _ h _ := toEquiv_injective <| DFunLike.ext' h

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