# 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

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

.

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

.