Counting a finite set by its fibers

Two Set.ncard forms of the familiar Finset estimates, upstreaming candidates:

• Set.ncard_le_mul_ncard_image: if every fiber of f on s has at most n elements, then s has at most n times as many elements as its image.
• Set.ncard_le_sum_ncard_fiber: a set on which a natural-number function takes values below T has at most as many elements as the sum of its fibers over 0, ..., T - 1.

theorem Set.ncard_le_mul_ncard_image {α : Type u_1} {β : Type u_2} {s : Set α} (hs : s.Finite) (f : α → β) (n : ℕ) (h : ∀ (b : β), (s ∩ f ⁻¹' {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_le_sum_ncard_fiber {α : Type u_1} {s : Set α} (hs : s.Finite) (f : α → ℕ) (T : ℕ) (hf : ∀ a ∈ s, f a < T) : s.ncard ≤ ∑ t ∈ Finset.range T, (s ∩ f ⁻¹' {t}).ncard

A finite set on which f takes values below T is no larger than the sum of its fibers over 0, ..., T - 1.

theorem Set.ncard_image_le_ncard_image_of_determines {α : 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 is determined by g on s, then f takes at most as many values on s as g.