Documentation

Mathlib.Data.Finset.Finsupp

Finitely supported product of finsets #

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.

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

Finitely supported product of finsets.

Equations
Instances For
    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 : ι), i sf 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 α) :
    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
    Instances For
      @[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 α) :
      Finset.card (Finsupp.pi f) = Finsupp.prod f fun i => ↑(Finset.card (f i))