symm_toHomotopyEquiv — Mathlib

English

The symmetry of a homeomorphism yields equality of the corresponding opposite homotopy equivalences.

Русский

Симметрия гомеоморфизма дает равенство соответствующих обратных гомотопических эквивалентностей.

LaTeX

$$$h.symm.toHomotopyEquiv = h.toHomotopyEquiv.symm$$$

Lean4

@[simp]
theorem symm_toHomotopyEquiv (h : X ≃ₜ Y) : h.symm.toHomotopyEquiv = h.toHomotopyEquiv.symm :=
  rfl

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