English
For x ≠ y, the swap x y has exactly two elements in its support.
Русский
Для x ≠ y перестановка swap x y имеет ровно два элемента в своей опоре.
LaTeX
$$$(\operatorname{swap}(x,y)).\operatorname{support}.card = 2$$$
Lean4
@[simp]
theorem card_support_eq_two {f : Perm α} : #f.support = 2 ↔ IsSwap f :=
by
constructor <;> intro h
· obtain ⟨x, t, hmem, hins, ht⟩ := card_eq_succ.1 h
obtain ⟨y, rfl⟩ := card_eq_one.1 ht
rw [mem_singleton] at hmem
refine ⟨x, y, hmem, ?_⟩
ext a
have key : ∀ b, f b ≠ b ↔ _ := fun b => by rw [← mem_support, ← hins, mem_insert, mem_singleton]
by_cases ha : f a = a
· have ha' := not_or.mp (mt (key a).mpr (not_not.mpr ha))
rw [ha, swap_apply_of_ne_of_ne ha'.1 ha'.2]
· have ha' := (key (f a)).mp (mt f.apply_eq_iff_eq.mp ha)
obtain rfl | rfl := (key a).mp ha
· rw [Or.resolve_left ha' ha, swap_apply_left]
· rw [Or.resolve_right ha' ha, swap_apply_right]
· obtain ⟨x, y, hxy, rfl⟩ := h
exact card_support_swap hxy
