# Definition of the `Finite`

typeclass #

This file defines a typeclass `Finite`

saying that `α : Sort*`

is finite. A type is `Finite`

if it
is equivalent to `Fin n`

for some `n`

. We also define `Infinite α`

as a typeclass equivalent to
`¬Finite α`

.

The `Finite`

predicate has no computational relevance and, being `Prop`

-valued, gets to enjoy proof
irrelevance -- it represents the mere fact that the type is finite. While the `Finite`

class also
represents finiteness of a type, a key difference is that a `Fintype`

instance represents finiteness
in a computable way: it gives a concrete algorithm to produce a `Finset`

whose elements enumerate
the terms of the given type. As such, one generally relies on congruence lemmas when rewriting
expressions involving `Fintype`

instances.

Every `Fintype`

instance automatically gives a `Finite`

instance, see `Fintype.finite`

, but not vice
versa. Every `Fintype`

instance should be computable since they are meant for computation. If it's
not possible to write a computable `Fintype`

instance, one should prefer writing a `Finite`

instance
instead.

## Main definitions #

## Implementation notes #

The definition of `Finite α`

is not just `Nonempty (Fintype α)`

since `Fintype`

requires
that `α : Type*`

, and the definition in this module allows for `α : Sort*`

. This means
we can write the instance `Finite.prop`

.

## Tags #

finite, fintype

A type is `Finite`

if it is in bijective correspondence to some `Fin n`

.

This is similar to `Fintype`

, but `Finite`

is a proposition rather than data.
A particular benefit to this is that `Finite`

instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite`

instances generally avoid the need for `Decidable`

instances.
One other notable difference is that `Finite`

allows there to be `Finite p`

instances
for all `p : Prop`

, which is not allowed by `Fintype`

due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)`

follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`

.
Implementation note: this is a reason `Finite α`

is not defined as `Nonempty (Fintype α)`

.

Every `Fintype`

instance provides a `Finite`

instance via `Finite.of_fintype`

.
Conversely, one can noncomputably create a `Fintype`

instance from a `Finite`

instance
via `Fintype.ofFinite`

. In a proof one might write

```
have := Fintype.ofFinite α
```

to obtain such an instance.

Do not write noncomputable `Fintype`

instances; instead write `Finite`

instances
and use this `Fintype.ofFinite`

interface.
The `Fintype`

instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite`

instead of `Fintype`

, unless definitions in the theorem statement
require `Fintype`

.
Definitions should prefer `Finite`

as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval`

sense.

## Instances

**Alias** of the reverse direction of `not_infinite_iff_finite`

.

**Alias** of the forward direction of `not_infinite_iff_finite`

.