Cardinality of a quotient fiber

Main results

• Finset.card_filter_div_eq_le: an injectively indexed quotient fiber has at most the divisor many members.

References

Adapted from Counting.lean at anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5.

theorem Finset.card_filter_div_eq_le {α : Type u_1} (s : Finset α) {f : α → ℕ} (hf : Set.InjOn f ↑s) {c : ℕ} (hc : 0 < c) (k : ℕ) : {x ∈ s | f x / c = k}.card ≤ c

At most c elements x of s have ⌊f x / c⌋ = k, if f is injective on s: their values lie in [kc, kc + c).