English
If E is a type and X is a finite subset of E, and F : E → Multiset L is a family of multisets, then the dependent function type ∀ x : X, { l ∈ F x | l ∈ F x } has a finite instance; i.e., there is a finite type for choosing, for each x in X, an element of L from F x.
Русский
Если E — множество, X ⊆ E — конечное, и F: E → Multiset L — семейство мультисет; тогда зависимая функция ∀ x : X, { l ∈ L | l ∈ F x } образует конечный тип.
LaTeX
$$$Fintype (\forall x : X, \{ l : L // l \in F x \})$$$
Lean4
/-- A technical finiteness result. -/
noncomputable def subtypeProd {E : Type*} {X : Set E} (hX : X.Finite) {L : Type*} (F : E → Multiset L) :
Fintype (∀ x : X, { l : L // l ∈ F x }) :=
@Pi.instFintype _ _ _ (Finite.fintype hX) _
