English
Given a finitely supported function f: i ↦ Finset(α i), one defines the finset π f of all finitely supported functions whose value at i lies in f(i).
Русский
Для конечной поддержки f : i ↦ Finset(α i) задаётся Finset π f всех конечноподдерживаемых функций, значение в i принадлежит f(i).
LaTeX
$$def pi (f : Π₀ i, Finset (α i)) : Finset (Π₀ i, α i) := f.support.dfinsupp f$$
Lean4
/-- Given a finitely supported function `f : Π₀ i, Finset (α i)`, one can define the finset
`f.pi` of all finitely supported functions whose value at `i` is in `f i` for all `i`. -/
def pi (f : Π₀ i, Finset (α i)) : Finset (Π₀ i, α i) :=
f.support.dfinsupp f
