symm_apply_eq

Mathlib.Algebra.Algebra.Equiv

URI: https://scilib.ai/kg/mathlib#AlgEquiv.symm_apply_eq

English

For any x,y, y = e.symm x if and only if e y = x; i.e. taking inverses corresponds to equality under the forward map.

Русский

Пусть y = e^{-1}(x); тогда e(y) = x; эквивалентно равенству.

LaTeX

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

Lean4

theorem symm_apply_eq (e : A₁ ≃ₐ[R] A₂) {x y} : e.symm x = y ↔ x = e y :=
  e.toEquiv.symm_apply_eq

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

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

Разделы

Аффилиация

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