coe_support_eq_set_support

Mathlib.GroupTheory.Perm.Support

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

English

If (swap x (f x) * f) y ≠ y, then f y ≠ y and y ≠ x.

Русский

Если (swap x (f x) · f) y ≠ y, то f y ≠ y и y ≠ x.

LaTeX

$$$$ (\mathrm{swap}(x, f(x))\cdot f)(y) \neq y \Rightarrow (f(y) \neq y \wedge y \neq x). $$$$

Lean4

theorem coe_support_eq_set_support (f : Perm α) : (f.support : Set α) = {x | f x ≠ x} :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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