coe_symm_toEquiv — Mathlib

English

The function obtained by applying the inverse of the underlying equivalence to e is the same as the inverse of the linear equivalence e.

Русский

Функция, полученная обращением к обратной базовой эквивалентности e, равна обратной линейной эквивалентности e.

LaTeX

$$$\\bigl(\\mathrm{toEquiv}(e)\\bigr)^{-1} = e^{-1}$ as functions$$

Lean4

@[simp]
theorem coe_symm_toEquiv : ⇑e.toEquiv.symm = e.symm :=
  rfl

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