# Finitely supported product of finsets #

This file defines the finitely supported product of finsets as a Finset (ι →₀ α).

## Main declarations #

• Finset.finsupp: Finitely supported product of finsets. s.finset t is the product of the t i over all i ∈ s.
• Finsupp.pi: f.pi is the finset of Finsupps whose i-th value lies in f i. This is the special case of Finset.finsupp where we take the product of the f i over the support of f.

## Implementation notes #

We make heavy use of the fact that 0 : Finset α is {0}. This scalar actions convention turns out to be precisely what we want here too.

def Finset.finsupp {ι : Type u_1} {α : Type u_2} [Zero α] (s : ) (t : ι) :
Finset (ι →₀ α)

Finitely supported product of finsets.

Equations
• s.finsupp t = Finset.map { toFun := , inj' := } (s.pi t)
Instances For
theorem Finset.mem_finsupp_iff {ι : Type u_1} {α : Type u_2} [Zero α] {s : } {f : ι →₀ α} {t : ι} :
f s.finsupp t f.support s is, f i t i
@[simp]
theorem Finset.mem_finsupp_iff_of_support_subset {ι : Type u_1} {α : Type u_2} [Zero α] {s : } {f : ι →₀ α} {t : ι →₀ } (ht : t.support s) :
f s.finsupp t ∀ (i : ι), f i t i

When t is supported on s, f ∈ s.finsupp t precisely means that f is pointwise in t.

@[simp]
theorem Finset.card_finsupp {ι : Type u_1} {α : Type u_2} [Zero α] (s : ) (t : ι) :
(s.finsupp t).card = is, (t i).card
def Finsupp.pi {ι : Type u_1} {α : Type u_2} [Zero α] (f : ι →₀ ) :
Finset (ι →₀ α)

Given a finitely supported function f : ι →₀ Finset α, one can define the finset f.pi of all finitely supported functions whose value at i is in f i for all i.

Equations
• f.pi = f.support.finsupp f
Instances For
@[simp]
theorem Finsupp.mem_pi {ι : Type u_1} {α : Type u_2} [Zero α] {f : ι →₀ } {g : ι →₀ α} :
g f.pi ∀ (i : ι), g i f i
@[simp]
theorem Finsupp.card_pi {ι : Type u_1} {α : Type u_2} [Zero α] (f : ι →₀ ) :
f.pi.card = f.prod fun (i : ι) => (f i).card