symm_apply

Mathlib.Algebra.Algebra.Equiv

URI: https://scilib.ai/kg/mathlib#AlgEquiv.Simps.symm_apply

English

The symmetric application map e.symm is the inverse function of the forward map e.

Русский

Симметричное применение это обратная функция по отношению к прямому отображению.

LaTeX

$$$\forall x, e^{-1}(x) = y \iff x = e(y)$$$

Lean4

/-- See Note [custom simps projection] -/
def symm_apply (e : A₁ ≃ₐ[R] A₂) : A₂ → A₁ :=
  e.symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru