Theorems · Theorem · group theory

Set.mem_fintype_sum

∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : Fintype ι] (f : ι → Set α) (a : α),
  a ∈ ∑ i, f i ↔ ∃ g, ∃ (_ : ∀ (i : ι), g i ∈ f i), ∑ i, g i = a

A version of Set.mem_finsetSum with a simpler RHS for sums over a Fintype.

Defined in

Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Cited by

0 results in Mathlib

Foundations

Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidFintype