mathlib3 documentation

data.finite.defs

Definition of the finite typeclass #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
@[class]
inductive finite (α : Sort u_1) :
Prop

A type is finite if it is in bijective correspondence to some fin n.

While this could be defined as nonempty (fintype α), it is defined in this way to allow there to be finite instances for propositions.

Instances of this typeclass
source
theorem finite_iff_exists_equiv_fin {α : Sort u_1} :
finite α ↔ ∃ (n : ℕ), nonempty (α ≃ fin n)
source
theorem finite.exists_equiv_fin (α : Sort u_1) [h : finite α] :
∃ (n : ℕ), nonempty (α ≃ fin n)
source
theorem finite.of_equiv {β : Sort u_2} (α : Sort u_1) [h : finite α] (f : α ≃ β) :
finite β
source
theorem equiv.finite_iff {α : Sort u_1} {β : Sort u_2} (f : α ≃ β) :
finite α ↔ finite β
source
theorem function.bijective.finite_iff {α : Sort u_1} {β : Sort u_2} {f : α → β} (h : function.bijective f) :
finite α ↔ finite β
source
theorem finite.of_bijective {α : Sort u_1} {β : Sort u_2} [finite α] {f : α → β} (h : function.bijective f) :
finite β
source
@[protected, instance]
def plift.finite {α : Sort u_1} [finite α] :
finite (plift α)
source
@[protected, instance]
def ulift.finite {α : Type v} [finite α] :
finite (ulift α)
source
@[class]
structure infinite (α : Sort u_3) :
Prop

A type is said to be infinite if it is not finite. Note that infinite α is equivalent to is_empty (fintype α) or is_empty (finite α).

Instances of this typeclass
source
@[simp]
theorem not_finite_iff_infinite {α : Sort u_1} :
¬finite α ↔ infinite α
source
@[simp]
theorem not_infinite_iff_finite {α : Sort u_1} :
¬infinite α ↔ finite α
source
theorem equiv.infinite_iff {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) :
infinite α ↔ infinite β
source
@[protected, instance]
def plift.infinite {α : Sort u_1} [infinite α] :
infinite (plift α)
source
@[protected, instance]
def ulift.infinite {α : Type v} [infinite α] :
infinite (ulift α)
source
theorem finite_or_infinite (α : Sort u_1) :
finite α ∨ infinite α
source
theorem not_finite (α : Sort u_1) [infinite α] [finite α] :
false
source
@[protected]
theorem finite.false {α : Sort u_1} [infinite α] (h : finite α) :
false
source
@[protected]
theorem infinite.false {α : Sort u_1} [finite α] (h : infinite α) :
false
source
theorem finite.of_not_infinite {α : Sort u_1} :
¬infinite α → finite α

Alias of the forward direction of not_infinite_iff_finite.

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

Alias of the reverse direction of not_infinite_iff_finite.