English
An induction principle for permutations: if a property holds for the identity and is preserved when composing with a nontrivial swap, it holds for all permutations.
Русский
Принцип индукции по перестановкам: если свойство верно для тождественной перестановки и сохраняется при умножении на неправая транспозицию, то верно для всех перестановок.
LaTeX
$$$ \\forall f, motive(1) \\land (\\forall f x y, x \\neq y \\to motive(f) \\to motive(swap x y * f)) \\,\\Rightarrow \\, motive(f) $$$
Lean4
/-- An induction principle for permutations. If `P` holds for the identity permutation, and
is preserved under composition with a non-trivial swap, then `P` holds for all permutations. -/
@[elab_as_elim]
theorem swap_induction_on [Finite α] {motive : Perm α → Prop} (f : Perm α) (one : motive 1)
(swap_mul : ∀ f x y, x ≠ y → motive f → motive (swap x y * f)) : motive f :=
by
cases nonempty_fintype α
obtain ⟨l, hl⟩ := (truncSwapFactors f).out
induction l generalizing f with
| nil => simp only [one, hl.left.symm, List.prod_nil]
| cons g l ih =>
rcases hl.2 g (by simp) with ⟨x, y, hxy⟩
rw [← hl.1, List.prod_cons, hxy.2]
exact swap_mul _ _ _ hxy.1 (ih _ ⟨rfl, fun v hv => hl.2 _ (List.mem_cons_of_mem _ hv)⟩)
