mathlib3 documentation

data.finset.finsupp

Finitely supported product of finsets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main declarations #

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.

source
@[protected]
noncomputable def finset.finsupp {ι : Type u_1} {α : Type u_2} [has_zero α] (s : finset ι) (t : ι → finset α) :
finset (ι →₀ α)

Finitely supported product of finsets.

Equations
source
theorem finset.mem_finsupp_iff {ι : Type u_1} {α : Type u_2} [has_zero α] {s : finset ι} {f : ι →₀ α} {t : ι → finset α} :
f ∈ s.finsupp t ↔ f.support ⊆ s ∧ ∀ (i : ι), i ∈ s → ⇑f i ∈ t i
source
@[simp]
theorem finset.mem_finsupp_iff_of_support_subset {ι : Type u_1} {α : Type u_2} [has_zero α] {s : finset ι} {f : ι →₀ α} {t : ι →₀ finset α} (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.

source
@[simp]
theorem finset.card_finsupp {ι : Type u_1} {α : Type u_2} [has_zero α] (s : finset ι) (t : ι → finset α) :
(s.finsupp t).card = s.prod (λ (i : ι), (t i).card)
source
noncomputable def finsupp.pi {ι : Type u_1} {α : Type u_2} [has_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
source
@[simp]
theorem finsupp.mem_pi {ι : Type u_1} {α : Type u_2} [has_zero α] {f : ι →₀ finset α} {g : ι →₀ α} :
g ∈ f.pi ↔ ∀ (i : ι), ⇑g i ∈ ⇑f i
source
@[simp]
theorem finsupp.card_pi {ι : Type u_1} {α : Type u_2} [has_zero α] (f : ι →₀ finset α) :
f.pi.card = f.prod (λ (i : ι), ↑((⇑f i).card))