toIso_inv — Mathlib

English

Let e: X ≃ Y be an isomorphism between types. Then the inverse of its associated isomorphism equals e.symm; i.e., e.toIso.inv = e.symm.

Русский

Пусть e: X ≃ Y — изоморфизм между типами. Тогда обратное изоморфирование, соответствующее e, равно e.symm; т.е. e.toIso.inv = e.symm.

LaTeX

$$$ e.toIso.inv = e.symm $$$

Lean4

@[simp]
theorem toIso_inv {e : X ≃ Y} : e.toIso.inv = e.symm :=
  rfl

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