Counting a finite set by its fibers

Set.ncard forms of the familiar Finset estimates.

Main results

• Set.ncard_eq_sum_ncard_fiberwise: a finite set mapped into a finset is the disjoint union of its fibers (Finset.card_eq_sum_card_fiberwise).
• Set.ncard_le_mul_ncard_image: a finite set whose fibers under f have at most n elements has at most n times as many elements as its image (Finset.card_le_mul_card_image).
• Set.ncard_image_le_ncard_image_of_factorsThrough: if f factors through g on s, then f takes at most as many values on s as g.
• Set.encard_lt_coe_iff_finite_ncard_lt: encard and ncard agree below a natural number (Set.encard_le_coe_iff_finite_ncard_le).

theorem Set.encard_lt_coe_iff_finite_ncard_lt {α : Type u_1} {s : Set α} {k : ℕ} : s.encard < ↑k ↔ s.Finite ∧ s.ncard < k

A set has fewer than k elements, counted with encard, exactly when it is finite with fewer than k elements counted with ncard.

theorem Set.ncard_eq_sum_ncard_fiberwise {α : Type u_1} {β : Type u_2} {s : Set α} (hs : s.Finite) {f : α → β} {t : Finset β} (H : MapsTo f s ↑t) : s.ncard = ∑ b ∈ t, {a : α | a ∈ s ∧ f a = b}.ncard

A finite set that f maps into the finset t is the disjoint union of its fibers over t.

theorem Set.ncard_le_mul_ncard_image {α : Type u_1} {β : Type u_2} {s : Set α} (hs : s.Finite) (f : α → β) (n : ℕ) (hn : ∀ b ∈ f '' s, {a : α | a ∈ s ∧ f a = b}.ncard ≤ n) : s.ncard ≤ n * (f '' s).ncard

A finite set whose fibers under f have at most n elements has at most n times as many elements as its image.

theorem Set.ncard_image_le_ncard_image_of_factorsThrough {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} (hs : s.Finite) {f : α → β} {g : α → γ} (h : ∀ a ∈ s, ∀ b ∈ s, g a = g b → f a = f b) : (f '' s).ncard ≤ (g '' s).ncard

If f factors through g on s, that is, f agrees on any two points of s at which g agrees, then f takes at most as many values on the finite set s as g does.