Theorems · Inductive type · combinatorics

Finite

Sort u_3 → Prop

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 ``lean 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.

Defined in

Mathlib.Data.Finite.Defs

Cited by

3,029 results in Mathlib

Foundations

Depth 0 from the axioms, rests on 1 definitions · uses no axioms