English
Let s be a finite set of indices and t(i) be a Finset for each i ∈ s. The finitely supported product over s, denoted s.dfinsupp t, is the Finset of all DFinsupps whose i-th component lies in t(i) for i ∈ s (and is zero outside s).
Русский
Пусть s — конечная подмножество индексов, и для каждого i∈s дано конечное множество t(i). Нормированное произведение над s, обозначаемое s.dfinsupp t, есть конечное множество DFinsupp-объектов, у которых i-я компонента принадлежит t(i) для i∈s (и равна нулю при i∉s).
LaTeX
$$$s.dfinsupp t \cong \prod_{i \in s} t(i)$$$
Lean4
/-- Finitely supported product of finsets. -/
def dfinsupp (s : Finset ι) (t : ∀ i, Finset (α i)) : Finset (Π₀ i, α i) :=
(s.pi t).map
⟨fun f => DFinsupp.mk s fun i => f i i.2,
by
refine (mk_injective _).comp fun f g h => ?_
ext i hi
convert congr_fun h ⟨i, hi⟩⟩
