Selecting submultisets with prescribed fibre masses

All selections are made in natural multiplicities, so coincident vector values are still allowed to occupy distinct positions.

theorem EGZ.Expansion.exists_subweight_of_mass_le {A : Type u_1} [Fintype A] (w : A → ℕ) {n : ℕ} (hn : n ≤ natMass w) : ∃ u ≤ w, natMass u = n

theorem EGZ.Expansion.exists_subweight_pushWeight {A : Type u_1} {B : Type u_2} [Fintype A] (π : A → B) (w : A → ℕ) (a : B → ℕ) (ha : a ≤ pushWeight π w) : ∃ u ≤ w, pushWeight π u = a

Every collection of fibre counts dominated by the available counts can be realized by a submultiset.

theorem EGZ.Expansion.pushWeight_add {A : Type u_1} {B : Type u_2} [Fintype A] (π : A → B) (u w : A → ℕ) : pushWeight π (u + w) = pushWeight π u + pushWeight π w

theorem EGZ.Expansion.pushWeight_sub {A : Type u_1} {B : Type u_2} [Fintype A] (π : A → B) {u w : A → ℕ} (hu : u ≤ w) : pushWeight π (w - u) = pushWeight π w - pushWeight π u

theorem EGZ.Expansion.pushWeight_sum {A : Type u_1} {B : Type u_2} {I : Type u_3} [Fintype A] (π : A → B) (s : Finset I) (w : I → A → ℕ) : pushWeight π (∑ i ∈ s, w i) = ∑ i ∈ s, pushWeight π (w i)