coe_fn_symm_mk — Mathlib

English

If an equivalence is constructed by mk with data f, g, l, r, then its inverse function coincides with g; i.e., the inverse map is g.

Русский

Если эквивокальная структура создаётся как mk с данными f, g, l, r, то её обратная функция совпадает с g; то есть обратное отображение равно g.

LaTeX

$$$((\\mathrm{Equiv.mk} f\\ g\\ l\\ r)^{-1}) = g.$$$

Lean4

@[simp]
theorem coe_fn_symm_mk (f : α → β) (g l r) : ((Equiv.mk f g l r).symm : β → α) = g :=
  rfl

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