coe_fn_symm_mk — Mathlib

English

Let e be a RelIso constructed from a pair (f, o) using RelIso.mk. Then the underlying function of the inverse RelIso equals the inverse function of f: the coercion of the symmetry is f.symm.

Русский

Пусть e — RelIso, полученный из пары (f, o) с помощью RelIso.mk. Тогда базовая функция обратного RelIso равна обратной функции f: приведение к функции симметрии даёт f.symm.

LaTeX

$$$$(\text{RelIso.mk}\ f\ o)^{-1} = f^{-1}.$$$

Lean4

@[simp]
theorem coe_fn_symm_mk (f o) : ((@RelIso.mk _ _ r s f @o).symm : β → α) = f.symm :=
  rfl

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