Theorems · Theorem · group theory

List.exists_pw_disjoint_with_card

∀ {α : Type u_2} [inst : Fintype α] {c : List ℕ},
  c.sum ≤ Fintype.card α → ∃ o, List.map List.length o = c ∧ (∀ s ∈ o, s.Nodup) ∧ List.Pairwise List.Disjoint o

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

Defined in

Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Cited by

1 results in Mathlib

Foundations

Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Fintype