pi — Mathlib · SciLib

English

Given f : ι →₀ Finset α, define the finset f.pi of all finitely supported functions whose value at i lies in f(i) for every i.

Русский

Дано f : ι →₀ Finset α. Определим множество f.pi всех функций с конечной опорой, удовлетворяющих условию f(i) элемент f(i) для каждого i.

LaTeX

$$$f.pi = f.support.finsupp f$$$

Lean4

/-- 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`. -/
def pi (f : ι →₀ Finset α) : Finset (ι →₀ α) :=
  f.support.finsupp f

Похожие утверждения