English
All DFunLike objects are finite provided the index α is finite, the fiber types β(i) are finite, and α has a DecidableEq.
Русский
Все объекты DFunLike конечно конечны при условии, что индекс α конечен, волокна β(i) конечно, и есть DecidableEq на α.
LaTeX
$$$[DecidableEq\ α] [Fintype\ α] [\forall i, Fintype(β(i))] \Rightarrow Fintype(F)$$$
Lean4
/-- All `DFunLike`s are finite if their domain and codomain are.
This is not an instance because specific `DFunLike` types might have a better-suited definition.
See also `DFunLike.finite`.
-/
noncomputable def fintype [DecidableEq α] [Fintype α] [∀ i, Fintype (β i)] : Fintype F :=
Fintype.ofInjective _ DFunLike.coe_injective
