# Finiteness of `FunLike`

types #

We show a type `F`

with a `FunLike F α β`

is finite if both `α`

and `β`

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

`FunLike.fintype`

is a definition stating all`FunLike`

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

is a lemma stating all`FunLike`

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

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

and`FunLike.finite`

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

, because dependent instances are harder to infer.

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

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 `FunLike`

s are finite if their domain and codomain are.

This is not an instance because specific `FunLike`

types might have a better-suited definition.

See also `FunLike.finite`

.

## Equations

- FunLike.fintype F = Fintype.ofInjective (fun f => ↑f) (_ : Function.Injective fun f => ↑f)

All `FunLike`

s are finite if their domain and codomain are.

Non-dependent version of `FunLike.fintype`

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

types might have a better-suited definition.

## Equations

All `FunLike`

s are finite if their domain and codomain are.

Non-dependent version of `FunLike.finite`

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