English
The support of the swap permutation is exactly the two-point set {x,y} when x ≠ y.
Русский
Опора перестановки swap x y равна точечному множеству {x,y}, если x ≠ y.
LaTeX
$$$\operatorname{supp}(\operatorname{swap} x y) = \{x,y\} \quad (x \ne y).$$$
Lean4
theorem support_swap_mul_swap {x y z : α} (h : List.Nodup [x, y, z]) : support (swap x y * swap y z) = { x, y, z } :=
by
simp only [List.not_mem_nil, and_true, List.mem_cons, not_false_iff, List.nodup_cons, and_self_iff,
List.nodup_nil] at h
push_neg at h
apply le_antisymm
· convert support_mul_le (swap x y) (swap y z) using 1
rw [support_swap h.left.left, support_swap h.right.left]
simp [-Finset.union_singleton]
· intro
simp only [mem_insert, mem_singleton]
rintro (rfl | rfl | rfl | _) <;>
simp [swap_apply_of_ne_of_ne, h.left.left, h.left.left.symm, h.left.right.symm, h.left.right.left.symm,
h.right.left.symm]
