symm_apply — Mathlib

English

For any equivalence e: α ≃ β, the function symm_apply e: β → α is identical to the inverse equivalence e^{-1}.

Русский

Для любой эквивалентности e: α ≃ β отображение symm_apply e: β → α совпадает с обратной эквивалентностью e^{-1}.

LaTeX

$$$\forall e:\alpha \simeq \beta,\ (symm\_apply\ e) = e^{-1}$$$

Lean4

/-- See Note [custom simps projection] -/
def symm_apply (e : α ≃ β) : β → α :=
  e.symm

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