Theorems · Definition · combinatorics

Finsupp.pi

{ι : Type u_1} → {α : Type u_2} → [inst : Zero α] → (ι →₀ 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.

Defined in

Mathlib.Data.Finset.Finsupp

Cited by

2 results in Mathlib

Foundations

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

Assumes

Zero