English
For f a permutation and x, the support of the product swap x with f(x) and f is the support of f with x removed, under suitable conditions.
Русский
Для перестановки f и элемента x опора произведения swap x (f x) ⋅ f равна опоре f, за исключением элемента x.
LaTeX
$$$\operatorname{supp}(\operatorname{swap} x (f x) \cdot f) = \operatorname{supp}(f) \setminus \{x\}$ под некоторыми допущениями.$$
Lean4
theorem support_swap_mul_eq (f : Perm α) (x : α) (h : f (f x) ≠ x) : (swap x (f x) * f).support = f.support \ { x } :=
by
by_cases hx : f x = x
· simp [hx, sdiff_singleton_eq_erase, notMem_support.mpr hx, erase_eq_of_notMem]
ext z
by_cases hzx : z = x
· simp [hzx]
by_cases hzf : z = f x
· simp [hzf, hx, h, swap_apply_of_ne_of_ne]
by_cases hzfx : f z = x
· simp [Ne.symm hzx, hzx, Ne.symm hzf, hzfx]
· simp [hzx, hzfx, f.injective.ne hzx, swap_apply_of_ne_of_ne]
