inv_eq_iff_eq

Mathlib.Algebra.Group.End

URI: https://scilib.ai/kg/mathlib#Equiv.Perm.inv_eq_iff_eq

English

For any f ∈ Perm α and x,y ∈ α, x = f^{-1} y iff f x = y.

Русский

Для любых f ∈ Perm α и x,y ∈ α верно: x = f^{-1} y, если и только если f x = y.

LaTeX

$$$\\\\forall {f : \\\\mathrm{Perm} \\\\alpha}, \\forall {x,y : \\\\alpha}, \\\\; x = f^{-1}(y) \\\\leftrightarrow f(x) = y$$$

Lean4

theorem inv_eq_iff_eq {f : Perm α} {x y : α} : f⁻¹ x = y ↔ x = f y :=
  f.symm_apply_eq

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

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

Разделы

Аффилиация

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