English
Given for all a a finite set t(a) of δ(a), one can form the finset of all functions taking values in t(a) for all a.
Русский
Задан набор для каждого a конечное множество t(a) элемента δ(a). Можно определить финсет всех функций, принимающих значения в t(a) для всех a.
LaTeX
$$$\\mathrm{piFinset}(t) : \\mathrm{Finset}(\\forall a, \\delta(a))$$$
Lean4
/-- Given for all `a : α` a finset `t a` of `δ a`, then one can define the
finset `Fintype.piFinset t` of all functions taking values in `t a` for all `a`. This is the
analogue of `Finset.pi` where the base finset is `univ` (but formally they are not the same, as
there is an additional condition `i ∈ Finset.univ` in the `Finset.pi` definition). -/
def piFinset (t : ∀ a, Finset (δ a)) : Finset (∀ a, δ a) :=
(Finset.univ.pi t).map ⟨fun f a => f a (mem_univ a), fun _ _ => by simp +contextual [funext_iff]⟩
