One-collision finite counting #
The additive enrichment proof reduces to a small finite pigeonhole lemma. If every fiber of a map has size at most two, and all nontrivial fibers have the same image, then identifying fibers loses at most one element.
theorem
Algebraic.Fusion.Arithmetic.Progress.Separated.Collision.card_sub_one_le_image
{Domain : Type u_1}
{Codomain : Type u_2}
[Fintype Domain]
[DecidableEq Domain]
[DecidableEq Codomain]
(map : Domain → Codomain)
(fiber_pair :
∀ {first second other : Domain},
first ≠ second → map first = map second → map other = map first → other = first ∨ other = second)
(collisions_same :
∀ {first second third fourth : Domain},
first ≠ second → map first = map second → third ≠ fourth → map third = map fourth → map third = map first)
:
A finite map with fibers of size at most two and at most one nontrivial
fiber loses at most one in the cardinality - 1 score.