eq_of_right

Mathlib.GroupTheory.Perm.Cycle.Basic

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

English

If f y = y and x ~_f y, then x = y.

Русский

Если y фиксирована перестановкой f и x, y лежат в одном цикле f, то x = y.

LaTeX

$$$\\forall f:\\mathrm{Perm}(\\alpha),\\; \\forall x,y:\\alpha,\\mathrm{SameCycle}(f\\ x\\ y) \\Rightarrow IsFixedPt(f,y) \\Rightarrow x=y.$$$

Lean4

theorem eq_of_right (h : SameCycle f x y) (hy : IsFixedPt f y) : x = y :=
  h.eq_of_left <| h.apply_eq_self_iff.2 hy

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

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

Разделы

Аффилиация

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