equiv_symm

Mathlib.Dynamics.FixedPoints.Basic

URI: https://scilib.ai/kg/mathlib#Function.IsFixedPt.equiv_symm

English

If x is fixed by a permutation e, then x is fixed by the inverse permutation e^{-1}.

Русский

Если x фиксирована перестановкой e, то она фиксирована и перестановкой e^{-1}.

LaTeX

$$$IsFixedPt e x \rightarrow IsFixedPt e^{-1} x$$$

Lean4

protected theorem equiv_symm (h : IsFixedPt e x) : IsFixedPt e.symm x :=
  h.to_leftInverse e.leftInverse_symm

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

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

Разделы

Аффилиация

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