ne_and_ne_of_swap_mul_apply_ne_self

Mathlib.GroupTheory.Perm.Support

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

← MathLib Explorer

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 ne_and_ne_of_swap_mul_apply_ne_self {f : Perm α} {x y : α} (hy : (swap x (f x) * f) y ≠ y) : f y ≠ y ∧ y ≠ x :=
  by
  simp only [swap_apply_def, mul_apply, f.injective.eq_iff] at *
  grind

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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