English
For multisets over a finite index, the sum equals the sup exactly when the summands are pairwise disjoint; equivalently, finitary sum equals supremum under disjointness conditions.
Русский
Для конечного индекса сумма равна верхней границе точно тогда, когда составляющие попарно дисjointны; иначе — не требует.
LaTeX
$$$i.sum f = i.sup f \iff \forall x \in i, \forall y \in i, x \neq y \Rightarrow Disjoint (f x) (f y)$$$
Lean4
theorem finset_sum_eq_sup_iff_disjoint [DecidableEq α] {i : Finset β} {f : β → Multiset α} :
i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y) := by
induction i using Finset.cons_induction_on with
| empty =>
simp only [Finset.notMem_empty, IsEmpty.forall_iff, imp_true_iff, Finset.sum_empty, Finset.sup_empty, bot_eq_zero]
| cons z i hz
hr =>
simp_rw [Finset.sum_cons hz, Finset.sup_cons, Finset.mem_cons, Multiset.sup_eq_union, forall_eq_or_imp, Ne,
not_true_eq_false, IsEmpty.forall_iff, true_and, imp_and, forall_and, ← hr, @eq_comm _ z]
have := fun x (H : x ∈ i) => ne_of_mem_of_not_mem H hz
simp +contextual only [this, not_false_iff, true_imp_iff]
simp_rw [← disjoint_finset_sum_left, ← disjoint_finset_sum_right, disjoint_comm, ← and_assoc, and_self_iff]
exact add_eq_union_left_of_le (Finset.sup_le fun x hx => le_sum_of_mem (mem_map_of_mem f hx))
