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 : Finset ι) (t : ι → Finset α) : Finset (ι →₀ α)

Finitely supported product of finsets.

Equations

• Finset.finsupp s t = Finset.map { toFun := Finsupp.indicator s, inj' := (_ : Function.Injective fun (f : (i : ι) → i ∈ s → α) => Finsupp.indicator s f) } (Finset.pi s t)

theorem Finset.mem_finsupp_iff {ι : Type u_1} {α : Type u_2} [Zero α] {s : Finset ι} {f : ι →₀ α} {t : ι → Finset α} : f ∈ Finset.finsupp s t ↔ f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i

@[simp]

theorem Finset.mem_finsupp_iff_of_support_subset {ι : Type u_1} {α : Type u_2} [Zero α] {s : Finset ι} {f : ι →₀ α} {t : ι →₀ Finset α} (ht : t.support ⊆ s) : f ∈ Finset.finsupp s ⇑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 : Finset ι) (t : ι → Finset α) : (Finset.finsupp s t).card = Finset.prod s fun (i : ι) => (t i).card

def Finsupp.pi {ι : Type u_1} {α : Type u_2} [Zero α] (f : ι →₀ Finset α) : 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

• Finsupp.pi f = Finset.finsupp f.support ⇑f

@[simp]

theorem Finsupp.mem_pi {ι : Type u_1} {α : Type u_2} [Zero α] {f : ι →₀ Finset α} {g : ι →₀ α} : g ∈ Finsupp.pi f ↔ ∀ (i : ι), g i ∈ f i

@[simp]

theorem Finsupp.card_pi {ι : Type u_1} {α : Type u_2} [Zero α] (f : ι →₀ Finset α) : (Finsupp.pi f).card = Finsupp.prod f fun (i : ι) => ↑(f i).card