Skip to content
Axiomatic Wiki

WLImages of finite sets are finite

Lemma·L25

Applying a function cannot grow a finite set.

If is finite and is a function, then the image is finite. In particular, if , then is finite.
In words
If A is finite and f is a function from A to B, then the image f[A] is finite. In particular, if f is surjective onto B, then B is finite.
Rests onF02F03F04F05F06F09F14A01A02A06A08
Never needed: F08 · F10 · F11 · F12 · F13 · A03 · A04 · A05 · A07 · A09 (computed from the citation graph, not asserted).

Proof

  1. 1
    Reduction to numeral domains. Let be a bijection (D034) and its inverse (L03). Then is a function (L02 (i)) and : indeed iff for some , iff for some , since is surjective onto (D007, D015). So it suffices to show: images of functions with domain a natural are finite.
  2. 2
    Induction on (T05 on , Separation). Base: a function on has empty image, (D007, D002, D033).
  3. 3
    Step: let and a function with domain . The restriction has domain , so its image is finite by hypothesis, say a bijection. The full image splits as , since every argument is in or equals (D006, D007).
  4. 4
    If : then by Extensionality, and is finite.
  5. 5
    If : extend by the pair exactly as in L24: is a bijection , injectivity of the extension because (L05 (i)), surjectivity by D006. So : finite. T05 gives .
  6. 6
    Surjective case: if is surjective onto , then (D015, Extensionality), which is finite.
∎

Remarks

Functions can merge elements but never create new ones, so images can only shrink or preserve size. The surjective special case is the one Lagrange's theorem needs: the map sending each group element to its coset is surjective onto the quotient, so a finite group has finitely many cosets.
Wikipedia ↗Set.Finite.image ↗

Used by

T13
Propose an edit1 published revision