mathlib documentation


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 fintype 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

theorem finite_iff_exists_equiv_fin {α : Sort u_1} :
finite α ∃ (n : ), nonempty fin n)
theorem finite.exists_equiv_fin (α : Sort u_1) [h : finite α] :
∃ (n : ), nonempty fin n)
theorem finite.of_equiv {β : Sort u_2} (α : Sort u_1) [h : finite α] (f : α β) :
theorem equiv.finite_iff {α : Sort u_1} {β : Sort u_2} (f : α β) :
theorem function.bijective.finite_iff {α : Sort u_1} {β : Sort u_2} {f : α → β} (h : function.bijective f) :
theorem finite.of_bijective {α : Sort u_1} {β : Sort u_2} [finite α] {f : α → β} (h : function.bijective f) :
@[protected, instance]
def plift.finite {α : Sort u_1} [finite α] :
@[protected, instance]
def ulift.finite {α : Type v} [finite α] :
theorem not_finite_iff_infinite {α : Sort u_1} :
theorem not_infinite_iff_finite {α : Sort u_1} :
theorem finite_or_infinite (α : Sort u_1) :
theorem not_finite (α : Sort u_1) [infinite α] [finite α] :
theorem finite.false {α : Sort u_1} [infinite α] (h : finite α) :
theorem infinite.false {α : Sort u_1} [finite α] (h : infinite α) :
theorem finite.of_not_infinite {α : Sort u_1} :
¬infinite αfinite α

Alias of the forward direction of not_infinite_iff_finite.

theorem finite.not_infinite {α : Sort u_1} :
finite α¬infinite α

Alias of the reverse direction of not_infinite_iff_finite.