Incoming sums are invariant under finite relabelling

theorem MagnitudeConjecture.incoming_sum_le_of_equiv {α : Type u} {β : Type v} [Fintype α] [Fintype β] (e : α ≃ β) (f : α → α → ℕ) (g : β → β → ℕ) (h : ∀ (a b : α), f a b = g (e a) (e b)) (B : ℕ) (hB : ∀ (b : β), ∑ a : β, g a b ≤ B) (b : α) : ∑ a : α, f a b ≤ B

Transport a uniform incoming-weight bound through a bijection of labels.