# Finiteness of `DFunLike`

types #

We show a type `F`

with a `DFunLike F α β`

is finite if both `α`

and `β`

are finite.
This corresponds to the following two pairs of declarations:

`DFunLike.fintype`

is a definition stating all`DFunLike`

s are finite if their domain and codomain are.`DFunLike.finite`

is a lemma stating all`DFunLike`

s are finite if their domain and codomain are.`FunLike.fintype`

is a non-dependent version of`DFunLike.fintype`

and`FunLike.finite`

is a non-dependent version of`DFunLike.finite`

, because dependent instances are harder to infer.

You can use these to produce instances for specific `DFunLike`

types.
(Although there might be options for `Fintype`

instances with better definitional behaviour.)
They can't be instances themselves since they can cause loops.

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`

.

## Equations

- DFunLike.fintype F = Fintype.ofInjective (fun (f : F) => ⇑f) ⋯

## Instances For

All `FunLike`

s are finite if their domain and codomain are.

Non-dependent version of `DFunLike.fintype`

that might be easier to infer.
This is not an instance because specific `FunLike`

types might have a better-suited definition.

## Equations

## Instances For

All `FunLike`

s are finite if their domain and codomain are.

Non-dependent version of `DFunLike.finite`

that might be easier to infer.
Can't be an instance because it can cause infinite loops.

## Equations

- FunLike.toDecidableEq a b = decidable_of_iff (⇑a = ⇑b) ⋯