English
For permutations σ, the statement that σ has exactly 3 moved points is equivalent to σ being a three-cycle.
Русский
Для перестановок σ равносильно тому, что у σ ровно три затронутые точки, и это значит, что σ — трёхцикл.
LaTeX
$$$#\mathrm{support}(\sigma) = 3 \iff σ.IsThreeCycle$$$
Lean4
theorem _root_.card_support_eq_three_iff : #σ.support = 3 ↔ σ.IsThreeCycle :=
by
refine ⟨fun h => ?_, IsThreeCycle.card_support⟩
by_cases h0 : σ.cycleType = 0
· rw [← sum_cycleType, h0, sum_zero] at h
exact (ne_of_lt zero_lt_three h).elim
obtain ⟨n, hn⟩ := exists_mem_of_ne_zero h0
by_cases h1 : σ.cycleType.erase n = 0
· rw [← sum_cycleType, ← cons_erase hn, h1, cons_zero, Multiset.sum_singleton] at h
rw [IsThreeCycle, ← cons_erase hn, h1, h, ← cons_zero]
obtain ⟨m, hm⟩ := exists_mem_of_ne_zero h1
rw [← sum_cycleType, ← cons_erase hn, ← cons_erase hm, Multiset.sum_cons, Multiset.sum_cons] at h
have : ∀ {k}, 2 ≤ m → 2 ≤ n → n + (m + k) = 3 → False := by omega
cases this (two_le_of_mem_cycleType (mem_of_mem_erase hm)) (two_le_of_mem_cycleType hn) h
