Z i ⊆ ∑ j in I, Z j

Stream: Is there code for X?

[Michael Stoll]

Is the following in mathlib?

example {a b} [add_comm_monoid b] {I : finset a} (Z : a → set b) {i : a} (h : i ∈ I) :
  Z i ⊆ ∑ j in I, Z j

If not, what is the best proof?

[Michael Stoll]

OK, I'm missing an important assumption: ∀ i ∈ I, (0 : b) ∈ Z i.

[Michael Stoll]

Maybe this makes it less likely to be in mathlib...

[Michael Stoll]

import algebra.big_operators.basic
open_locale big_operators

lemma zero_in_sum_of_zero_mem_summands {a b} [add_comm_monoid b] {I : finset a} (Z : a → set b)
  (h : ∀ i ∈ I, (0 : b) ∈ Z i) : (0 : b) ∈  ∑ j in I, Z j :=
finset.sum_induction _ _ (λ a b ha hb, set.mem_add.mpr ⟨0, 0, ha, hb, zero_add 0⟩)
  (set.mem_zero.mpr rfl) h

lemma set_subset_sum_of_zero_mem_summands {a b} [add_comm_monoid b] {I : finset a} (Z : a → set b)
  {i : a} (hi : i ∈ I) (h : ∀ i ∈ I, (0 : b) ∈ Z i) :
  Z i ⊆ ∑ j in I, Z j :=
begin
  intros z hz,
  rw [finset.sum_eq_add_sum_diff_singleton hi Z, set.mem_add],
  exact ⟨z, 0, hz, zero_in_sum_of_zero_mem_summands Z (λ i H, h i $ (finset.mem_sdiff.mp H).1),
          add_zero z⟩,
end

[Eric Wieser]

docs#set.mem_finset_sum is probably helpful

[Yaël Dillies]

There are lemmas like docs#set.multiset_sum_subset_multiset_sum that are quite close. But it seems we don't have your exact statement.

[Michael Stoll]

Eric Wieser said:

docs#set.mem_finset_sum is probably helpful

Indeed. Thanks!