symm — Mathlib

English

Inverse of a homeomorphism is a homeomorphism between the opposite spaces.

Русский

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

LaTeX

$$$$ h : X \simeq_t Y \quad\Rightarrow\quad h^{\mathrm{symm}} : Y \simeq_t X. $$$$

Lean4

/-- Inverse of a homeomorphism. -/
@[symm]
protected def symm (h : X ≃ₜ Y) : Y ≃ₜ X
    where
  continuous_toFun := h.continuous_invFun
  continuous_invFun := h.continuous_toFun
  toEquiv := h.toEquiv.symm

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