Counting distinct labels with shifts in a bounded window

theorem MagnitudeConjecture.GradedInterval.sigmaFinset_label_shift_injective {ι : Type u_1} (F : ι → Finset ℤ) : Function.Injective fun (a : (i : ι) × ↥(F i)) => (a.fst, ↑a.snd)

Forgetting membership proofs preserves distinct finite-label shifts.

theorem MagnitudeConjecture.GradedInterval.card_le_of_label_shift_window {ι : Type u_1} {α : Type u_2} [Fintype ι] [Fintype α] (label : α → ι) (shift : α → ℤ) (hinj : Function.Injective fun (a : α) => (label a, shift a)) (t : ℤ) (h : ℕ) (hwindow : ∀ (a : α), t ≤ shift a ∧ shift a ≤ t + ↑h) : Fintype.card α ≤ Fintype.card ι * (h + 1)

A family uniquely determined by a finite label and an integer shift has at most card ι * (h + 1) members in a window of width h.