English
There is a general induction principle for permutations by cycles: for Finite β, if a property P holds for the identity, for every IsCycle permutation, and if P is preserved under products of disjoint IsCycle permutations, then P holds for every permutation.
Русский
Существует общий принцип индукции по циклаm для перестановок: для конечного β, если свойство P верно для тождества, для каждой IsCycle перестановки и если P сохраняется под произведением непересекающихся IsCycle перестановок, то P верно для любой перестановки.
LaTeX
$$$[\text{Finite } \beta] \; (P:\mathrm{Perm}(\beta)\to \mathrm{Prop}) \; \Rightarrow \; P(\sigma) \;\text{если } P(1) \text{ и } (\forall \tau,\tau.IsCycle \to P(\tau)) \text{ и } (\forall \sigma,\tau,\mathrm{Disjoint}(\sigma,\tau) \to \tau.IsCycle \to P(\sigma) \to P(\tau) \to P(\sigma*\tau)).$$$
Lean4
/-- For any `c : List ℕ` whose sum is at most `Fintype.card α`,
we can find `o : List (List α)` whose members have no duplicate,
whose lengths given by `c`, and which are pairwise disjoint -/
theorem exists_pw_disjoint_with_card {α : Type*} [Fintype α] {c : List ℕ} (hc : c.sum ≤ Fintype.card α) :
∃ o : List (List α), o.map length = c ∧ (∀ s ∈ o, s.Nodup) ∧ Pairwise List.Disjoint o :=
by
let klift (n : ℕ) (hn : n < Fintype.card α) : Fin (Fintype.card α) := (⟨n, hn⟩ : Fin (Fintype.card α))
let klift' (l : List ℕ) (hl : ∀ a ∈ l, a < Fintype.card α) : List (Fin (Fintype.card α)) := List.pmap klift l hl
have hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α :=
by
intro l hl n hn
apply lt_of_lt_of_le _ hc
rw [← mem_mem_ranges_iff_lt_sum]
exact ⟨l, hl, hn⟩
let l := (ranges c).pmap klift' hc'_lt
have hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), (klift' a (hc'_lt a ha)).map Fin.valEmbedding = a :=
by
intro a ha
conv_rhs => rw [← List.map_id a]
rw [List.map_pmap]
simp [klift, Fin.valEmbedding_apply, List.pmap_eq_map, List.map_id']
use l.map (List.map (Fintype.equivFin α).symm)
constructor
· -- length
rw [← ranges_length c]
simp only [l, klift', map_pmap, length_pmap, pmap_eq_map]
constructor
· -- nodup
intro s
rw [mem_map]
rintro ⟨t, ht, rfl⟩
apply Nodup.map (Equiv.injective _)
obtain ⟨u, hu, rfl⟩ := mem_pmap.mp ht
apply Nodup.of_map
rw [hl u hu]
exact ranges_nodup hu
· -- pairwise disjoint
refine
Pairwise.map _ (fun s t ↦ disjoint_map (Equiv.injective _))
?_
-- List.Pairwise List.disjoint l
apply Pairwise.pmap (List.ranges_disjoint c)
intro u hu v hv huv
apply disjoint_pmap
· intro a a' ha ha' h
simpa only [klift, Fin.mk_eq_mk] using h
exact huv
