symm — Mathlib

English

If e: α ≃ β is given, there exists an inverse equivalence e^{-1}: β ≃ α whose forward map is e^{-1} (the inverse of e) and whose inverse is e.

Русский

Пусть дано e: α ≃ β. Существует обратная эквивалентность e^{-1}: β ≃ α, у которой отображение впереди равно обратному отображению e, а обратное отображение — e.

LaTeX

$$$\exists f:\beta \simeq \alpha,\ f.toFun = e.invFun \land f.invFun = e.toFun$$$

Lean4

/-- Inverse of an equivalence `e : α ≃ β`. -/
@[symm]
protected def symm (e : α ≃ β) : β ≃ α :=
  ⟨e.invFun, e.toFun, e.right_inv, e.left_inv⟩

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