English
A transposition (swap a b) acts as a 2-cycle on {a,b} and fixes nothing else in that set.
Русский
Transposition (swap a b) образует 2-цикл на {a,b} и никак не действует на остальные элементы этого набора.
LaTeX
$$$\\forall a \\neq b, \\; (\\mathrm{swap}\\ a\\ b).IsCycleOn \\{a,b\\}.$$$
Lean4
theorem isCycleOn_swap [DecidableEq α] (hab : a ≠ b) : (swap a b).IsCycleOn { a, b } :=
⟨bijOn_swap (by simp) (by simp), fun x hx y hy =>
by
rw [Set.mem_insert_iff, Set.mem_singleton_iff] at hx hy
obtain rfl | rfl := hx <;> obtain rfl | rfl := hy
· exact ⟨0, by rw [zpow_zero, coe_one, id]⟩
· exact ⟨1, by rw [zpow_one, swap_apply_left]⟩
· exact ⟨1, by rw [zpow_one, swap_apply_right]⟩
· exact ⟨0, by rw [zpow_zero, coe_one, id]⟩⟩
