English
In a finite β, for any property P on Permutations, if P holds for the identity, P holds for every IsCycle permutation, and P is preserved under products of disjoint cycles, then P holds for every permutation.
Русский
Для конечного β и любой свойствa P над перестановками, если выполняются: P(1) и P для каждой IsCycle, и P сохраняется под произведением дисjunktных циклов, то P выполняется для любой перестановки.
LaTeX
$$$\forall \beta\,[\text{Finite }\beta]\; \forall P:\mathrm{Perm}(\beta)\to \mathrm{Prop},\; \forall \sigma:\mathrm{Perm}(\beta),\; P(1) \to (\forall \tau,\tau.IsCycle \to P(\tau)) \\to (\forall \sigma,\tau,\mathrm{Disjoint}(\sigma,\tau) \to \mathrm{IsCycle}(\sigma) \to P(\sigma) \to P(\tau) \to P(\sigma*\tau)) \to P(\sigma)$$$
Lean4
@[elab_as_elim]
theorem cycle_induction_on [Finite β] (P : Perm β → Prop) (σ : Perm β) (base_one : P 1)
(base_cycles : ∀ σ : Perm β, σ.IsCycle → P σ)
(induction_disjoint : ∀ σ τ : Perm β, Disjoint σ τ → IsCycle σ → P σ → P τ → P (σ * τ)) : P σ :=
by
cases nonempty_fintype β
suffices ∀ l : List (Perm β), (∀ τ : Perm β, τ ∈ l → τ.IsCycle) → l.Pairwise Disjoint → P l.prod by
classical
let x := σ.truncCycleFactors.out
exact (congr_arg P x.2.1).mp (this x.1 x.2.2.1 x.2.2.2)
intro l
induction l with
| nil => exact fun _ _ => base_one
| cons σ l ih =>
intro h1 h2
rw [List.prod_cons]
exact
induction_disjoint σ l.prod (disjoint_prod_right _ (List.pairwise_cons.mp h2).1) (h1 _ List.mem_cons_self)
(base_cycles σ (h1 σ List.mem_cons_self)) (ih (fun τ hτ => h1 τ (List.mem_cons_of_mem σ hτ)) h2.of_cons)
