symmEquiv — Mathlib

English

There is a natural equivalence between the type of equivalences α ≃ β and the type of equivalences β ≃ α given by taking inverses.

Русский

Существует естественное ортогональное взаимнооднозначное соответствие между типами эквивалентностей α ≃ β и β ≃ α, задаваемое взятием обратной эквивалентности.

LaTeX

$$$\text{symmEquiv} (\alpha, \beta) : (\alpha \simeq \beta) \simeq (\beta \simeq \alpha)$$$

Lean4

/-- `Equiv.symm` defines an equivalence between `α ≃ β` and `β ≃ α`. -/
@[simps! (attr := grind =)]
def symmEquiv (α β : Sort*) : (α ≃ β) ≃ (β ≃ α) where
  toFun := .symm
  invFun := .symm

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