perm_inv

Mathlib.Dynamics.FixedPoints.Basic

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

English

If x is a fixed point of e, then x is fixed by e^{-1}.

Русский

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

LaTeX

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

Lean4

protected theorem perm_inv (h : IsFixedPt e x) : IsFixedPt (⇑e⁻¹) x :=
  h.equiv_symm

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

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

Разделы

Аффилиация

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