Skip to content
Axiomatic Wiki
Lemma·L27

Counting a partition of equal classes

k boxes with m things each: k times m things in total.

Let be a partition of a set , and . If and every satisfies , then so is finite with , with from D033.
In words
For natural numbers k and m: if a set is split into k classes and every class has exactly m elements, then the whole set is equinumerous with k times m, so it is finite with k times m elements.
Rests onF02F03F04F05F06F08F09F11F12F14A01A02A06A08
Never needed: F10 · F13 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).

Proof

  1. 1
    We induct on , quantifying over everything else: let be the set of such that for every set and partition of with and all classes , one has (Separation; is fixed throughout).
  2. 2
    Base, : a bijection leaves empty: any would need a value in (D002). So (D023, D004: nothing has a member of a member of ). And by Claim A of L11 and the empty bijection. So .
  3. 3
    Step: let , and let partition with all classes . Choose a bijection onto : by L03 there is a bijection . Let (defined since , L15 (vi)), (D009) and (D004).
  4. 4
    : the restriction is injective and its image is : every equals for exactly one (bijectivity), and iff iff (D006: and leave ). So is a bijection , and its inverse is a bijection (L03): .
  5. 5
    is a partition of : its members are non-empty and pairwise disjoint because those of are (D023), and by definition of .
  6. 6
    , disjointly: every lies in some class (covering); if then , otherwise and ; conversely and . So by Extensionality. Disjointness: if , then for some , and with , contradicting pairwise disjointness of (D008, negation).
  7. 7
    Count: by the induction hypothesis applied to : , so is finite with ; and gives (D035, L23). L26 on the disjoint pair: the last step by Claim B of L11 read right to left. So and ; T05 finishes.
∎

Remarks

Multiplication as repeated addition, upgraded to sets: boxes of marbles hold marbles. The statement quantifies over all pairs inside the induction: peeling off one class changes both the set and the partition, so the induction hypothesis must be portable. This is the counting engine of Lagrange's theorem, where the boxes are the cosets of a subgroup, all of size by L30.
Wikipedia ↗Finset.card_biUnion ↗

Used by

T13
Propose an edit1 published revision