English
Given a finite set s of indices and for each a ∈ s a finite set t(a) of β(a), the dependent product Finset s.π t is the Finset of all partial functions on s that assign to each a ∈ s a value in t(a).
Русский
Пусть s—конечное множество индексов, и для каждого a ∈ s задано конечное множество t(a) в β(a). Тогда Finset π s t представляет собой множество частичных функций на s, где каждому a ∈ s сопоставляется элемент из t(a).
LaTeX
$$$ s.\\pi t = \\{ f : (a ∈ s) \\to \\beta(a) \\mid \\forall a ∈ s, f(a) ∈ t(a) \\}$$$
Lean4
/-- Given a finset `s` of `α` and for all `a : α` a finset `t a` of `δ a`, then one can define the
finset `s.pi t` of all functions defined on elements of `s` taking values in `t a` for `a ∈ s`.
Note that the elements of `s.pi t` are only partially defined, on `s`. -/
def pi (s : Finset α) (t : ∀ a, Finset (β a)) : Finset (∀ a ∈ s, β a) :=
⟨s.1.pi fun a => (t a).1, s.nodup.pi fun a _ => (t a).nodup⟩
