Mathlib.Data.Finite.Defs

Module docstring

{"# 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

Finite α denotes that α is a finite type.
Infinite α denotes that α is an infinite type.
Set.Finite : Set α → Prop
Set.Infinite : Set α → Prop
Set.toFinite to prove Set.Finite for a Set from a Finite instance.

Implementation notes

This file defines both the type-level Finite class and the set-level Set.Finite definition.

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.

A finite set is defined to be a set whose coercion to a type has a Finite instance.

There are two components to finiteness constructions. The first is Fintype instances for each construction. This gives a way to actually compute a Finset that represents the set, and these may be accessed using set.toFinset. This gets the Finset in the correct form, since otherwise Finset.univ : Finset s is a Finset for the subtype for s. The second component is \"constructors\" for Set.Finite that give proofs that Fintype instances exist classically given other Set.Finite proofs. Unlike the Fintype instances, these do not use any decidability instances since they do not compute anything.

Tags

finite, fintype, finite sets ","### Finite sets ","### Infinite sets "}

Finite classInductive

(α : Sort*) : Prop

Full source

/-- 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.
-/
class inductive Finite (α : Sort*) : Prop
  | intro {n : ℕ} : α ≃ Fin n → Finite _

Finite Type

Informal description

A type $\alpha$ is called *finite* if there exists a natural number $n$ such that $\alpha$ is in bijective correspondence with the canonical type $\mathrm{Fin}\ n$ with $n$ elements. This is a propositional property (a `Prop`-valued class) that represents the mere fact that a type is finite, without providing any computational content. Unlike `Fintype`, which requires computable enumeration of elements, `Finite` can be used even for `Prop`-valued types and avoids decidability assumptions.

finite_iff_exists_equiv_fin theorem

{α : Sort*} : Finite α ↔ ∃ n, Nonempty (α ≃ Fin n)

Full source

theorem finite_iff_exists_equiv_fin {α : Sort*} : FiniteFinite α ↔ ∃ n, Nonempty (α ≃ Fin n) :=
  ⟨fun ⟨e⟩ => ⟨_, ⟨e⟩⟩, fun ⟨_, ⟨e⟩⟩ => ⟨e⟩⟩

Characterization of Finite Types via Bijection with Finite Ordinals

Informal description

A type $\alpha$ is finite if and only if there exists a natural number $n$ such that $\alpha$ is in bijective correspondence with the finite type $\mathrm{Fin}\ n$ (the type of natural numbers less than $n$).

Finite.exists_equiv_fin theorem

(α : Sort*) [h : Finite α] : ∃ n : ℕ, Nonempty (α ≃ Fin n)

Full source

theorem Finite.exists_equiv_fin (α : Sort*) [h : Finite α] : ∃ n : ℕ, Nonempty (α ≃ Fin n) :=
  finite_iff_exists_equiv_fin.mp h

Existence of Bijection with Finite Ordinals for Finite Types

Informal description

For any type $\alpha$ that is finite (i.e., has a `Finite` instance), there exists a natural number $n$ such that $\alpha$ is in bijective correspondence with the finite ordinal type $\mathrm{Fin}\ n$.

Finite.of_equiv theorem

(α : Sort*) [h : Finite α] (f : α ≃ β) : Finite β

Full source

theorem Finite.of_equiv (α : Sort*) [h : Finite α] (f : α ≃ β) : Finite β :=
  let ⟨e⟩ := h; ⟨f.symm.trans e⟩

Finite Types are Preserved under Equivalence

Informal description

Let $\alpha$ and $\beta$ be types, and suppose $\alpha$ is finite. If there exists a bijection $f : \alpha \simeq \beta$, then $\beta$ is also finite.

Equiv.finite_iff theorem

(f : α ≃ β) : Finite α ↔ Finite β

Full source

theorem Equiv.finite_iff (f : α ≃ β) : FiniteFinite α ↔ Finite β :=
  ⟨fun _ => Finite.of_equiv _ f, fun _ => Finite.of_equiv _ f.symm⟩

Finite Types are Equivalent under Bijection

Informal description

Given a bijection $f : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, the type $\alpha$ is finite if and only if $\beta$ is finite.

Function.Bijective.finite_iff theorem

{f : α → β} (h : Bijective f) : Finite α ↔ Finite β

Full source

theorem Function.Bijective.finite_iff {f : α → β} (h : Bijective f) : FiniteFinite α ↔ Finite β :=
  (Equiv.ofBijective f h).finite_iff

Finiteness is Preserved under Bijection: $\text{Finite}(\alpha) \leftrightarrow \text{Finite}(\beta)$

Informal description

For any function $f : \alpha \to \beta$, if $f$ is bijective (both injective and surjective), then the type $\alpha$ is finite if and only if the type $\beta$ is finite.

Finite.ofBijective theorem

[Finite α] {f : α → β} (h : Bijective f) : Finite β

Full source

theorem Finite.ofBijective [Finite α] {f : α → β} (h : Bijective f) : Finite β :=
  h.finite_iff.mp ‹_›

Finiteness Preservation under Bijection: $\text{Finite}(\alpha) \to \text{Finite}(\beta)$

Informal description

If $\alpha$ is a finite type and there exists a bijective function $f : \alpha \to \beta$, then $\beta$ is also a finite type.

Finite.nonempty_decidableEq theorem

[Finite α] : Nonempty (DecidableEq α)

Full source

theorem Finite.nonempty_decidableEq [Finite α] : Nonempty (DecidableEq α) :=
  let ⟨_n, ⟨e⟩⟩ := Finite.exists_equiv_fin α; ⟨e.decidableEq⟩

Existence of Decidable Equality for Finite Types

Informal description

For any finite type $\alpha$, there exists a decidable equality predicate on $\alpha$.

instFinitePLift instance

[Finite α] : Finite (PLift α)

Full source

instance [Finite α] : Finite (PLift α) :=
  Finite.of_equiv α Equiv.plift.symm

Finiteness of Lifted Types

Informal description

For any finite type $\alpha$, the lifted type $\mathrm{PLift}\,\alpha$ is also finite.

instFiniteULift instance

{α : Type v} [Finite α] : Finite (ULift.{u} α)

Full source

instance {α : Type v} [Finite α] : Finite (ULift.{u} α) :=
  Finite.of_equiv α Equiv.ulift.symm

Finiteness is Preserved under Universe Lifting

Informal description

For any type $\alpha$ in universe `Type v`, if $\alpha$ is finite, then its universe-lifted version `ULift.{u} α` (where `u` is another universe) is also finite.

Infinite structure

(α : Sort*)

Full source

/-- A type is said to be infinite if it is not finite. Note that `Infinite α` is equivalent to
`IsEmpty (Fintype α)` or `IsEmpty (Finite α)`. -/
class Infinite (α : Sort*) : Prop where
  /-- assertion that `α` is `¬Finite` -/
  not_finite : ¬Finite α

Infinite type

Informal description

A type `α` is said to be infinite if it is not finite. This is equivalent to the nonexistence of a bijection between `α` and `Fin n` for any natural number `n`. The structure `Infinite α` serves as a typeclass representing this property.

not_finite_iff_infinite theorem

: ¬Finite α ↔ Infinite α

Full source

@[simp]
theorem not_finite_iff_infinite : ¬Finite α¬Finite α ↔ Infinite α :=
  ⟨Infinite.mk, fun h => h.1⟩

Equivalence of Non-Finiteness and Infiniteness

Informal description

A type $\alpha$ is not finite if and only if it is infinite. That is, $\neg \text{Finite}(\alpha) \leftrightarrow \text{Infinite}(\alpha)$.

not_infinite_iff_finite theorem

: ¬Infinite α ↔ Finite α

Full source

@[simp]
theorem not_infinite_iff_finite : ¬Infinite α¬Infinite α ↔ Finite α :=
  not_finite_iff_infinite.not_right.symm

Equivalence of Non-Infiniteness and Finiteness

Informal description

A type $\alpha$ is not infinite if and only if it is finite, i.e., $\neg \text{Infinite}(\alpha) \leftrightarrow \text{Finite}(\alpha)$.

Equiv.infinite_iff theorem

(e : α ≃ β) : Infinite α ↔ Infinite β

Full source

theorem Equiv.infinite_iff (e : α ≃ β) : InfiniteInfinite α ↔ Infinite β :=
  not_finite_iff_infinite.symm.trans <| e.finite_iff.not.trans not_finite_iff_infinite

Infinite Types are Equivalent under Bijection

Informal description

Given a bijection $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, the type $\alpha$ is infinite if and only if $\beta$ is infinite.

instInfinitePLift instance

[Infinite α] : Infinite (PLift α)

Full source

instance [Infinite α] : Infinite (PLift α) :=
  Equiv.plift.infinite_iff.2 ‹_›

Lifted Infinite Types Remain Infinite

Informal description

For any infinite type $\alpha$, the lifted type $\text{PLift}\,\alpha$ is also infinite.

instInfiniteULift instance

{α : Type v} [Infinite α] : Infinite (ULift.{u} α)

Full source

instance {α : Type v} [Infinite α] : Infinite (ULift.{u} α) :=
  Equiv.ulift.infinite_iff.2 ‹_›

Lifted Infinite Types Remain Infinite

Informal description

For any infinite type $\alpha$ and any universe level $u$, the lifted type $\mathrm{ULift}\{u\} \alpha$ is also infinite.

finite_or_infinite theorem

(α : Sort*) : Finite α ∨ Infinite α

Full source

theorem finite_or_infinite (α : Sort*) : FiniteFinite α ∨ Infinite α :=
  or_iff_not_imp_left.2 not_finite_iff_infinite.1

Every Type is Finite or Infinite

Informal description

For any type $\alpha$, either $\alpha$ is finite or $\alpha$ is infinite.

not_finite theorem

(α : Sort*) [Infinite α] [Finite α] : False

Full source

/-- `Infinite α` is not `Finite` -/
theorem not_finite (α : Sort*) [Infinite α] [Finite α] : False :=
  @Infinite.not_finite α ‹_› ‹_›

Infinite and Finite Types are Mutually Exclusive

Informal description

For any type $\alpha$, if $\alpha$ is both infinite and finite, then we obtain a contradiction (False).

Finite.false theorem

[Infinite α] (_ : Finite α) : False

Full source

protected theorem Finite.false [Infinite α] (_ : Finite α) : False :=
  not_finite α

Contradiction from Simultaneous Finiteness and Infiniteness

Informal description

For any type $\alpha$, if $\alpha$ is infinite and finite simultaneously, then we obtain a contradiction (False).

Infinite.false theorem

[Finite α] (_ : Infinite α) : False

Full source

protected theorem Infinite.false [Finite α] (_ : Infinite α) : False :=
  @Infinite.not_finite α ‹_› ‹_›

Contradiction from Simultaneous Finiteness and Infiniteness

Informal description

For any type $\alpha$, if $\alpha$ is finite and infinite simultaneously, then we obtain a contradiction (False).

Bool.instFinite instance

: Finite Bool

Full source

instance Bool.instFinite : Finite Bool := .intro finTwoEquiv.symm

Finiteness of the Boolean Type

Informal description

The Boolean type `Bool` is finite.

Prop.instFinite instance

: Finite Prop

Full source

instance Prop.instFinite : Finite Prop := .of_equiv _ Equiv.propEquivBool.symm

Finiteness of the Proposition Type

Informal description

The type of propositions `Prop` is finite.

Set.Finite definition

(s : Set α) : Prop

Full source

/-- A set is finite if the corresponding `Subtype` is finite,
i.e., if there exists a natural `n : ℕ` and an equivalence `s ≃ Fin n`. -/
protected def Finite (s : Set α) : Prop := Finite s

Finite set

Informal description

A set $s$ over a type $\alpha$ is called *finite* if the corresponding subtype (i.e., the type of elements belonging to $s$) is finite, meaning there exists a natural number $n$ and a bijection between $s$ and the canonical type with $n$ elements $\mathrm{Fin}\ n$.

Set.finite_coe_iff theorem

{s : Set α} : Finite s ↔ s.Finite

Full source

theorem finite_coe_iff {s : Set α} : FiniteFinite s ↔ s.Finite := .rfl

Equivalence of Finite Type and Finite Set for Subtypes

Informal description

For any set $s$ over a type $\alpha$, the type corresponding to $s$ (i.e., the subtype of elements in $s$) is finite if and only if $s$ is a finite set.

Set.toFinite theorem

(s : Set α) [Finite s] : s.Finite

Full source

/-- Constructor for `Set.Finite` using a `Finite` instance. -/
theorem toFinite (s : Set α) [Finite s] : s.Finite := ‹_›

Finite Type Implies Finite Set

Informal description

For any set $s$ over a type $\alpha$, if the type corresponding to $s$ (i.e., the subtype of elements in $s$) is finite, then $s$ is a finite set.

Set.Finite.to_subtype theorem

{s : Set α} (h : s.Finite) : Finite s

Full source

/-- Projection of `Set.Finite` to its `Finite` instance.
This is intended to be used with dot notation.
See also `Set.Finite.Fintype` and `Set.Finite.nonempty_fintype`. -/
protected theorem Finite.to_subtype {s : Set α} (h : s.Finite) : Finite s := h

Finite Set Implies Finite Subtype

Informal description

For any set $s$ over a type $\alpha$, if $s$ is finite (i.e., $s.\text{Finite}$ holds), then the corresponding subtype of elements in $s$ is finite (i.e., $\text{Finite}\ s$ holds).

Set.Infinite definition

(s : Set α) : Prop

Full source

/-- A set is infinite if it is not finite.

This is protected so that it does not conflict with global `Infinite`. -/
protected def Infinite (s : Set α) : Prop :=
  ¬s.Finite

Infinite set

Informal description

A set $s$ over a type $\alpha$ is called *infinite* if it is not finite, meaning there does not exist a natural number $n$ and a bijection between $s$ and the canonical type with $n$ elements $\mathrm{Fin}\ n$.

Set.not_infinite theorem

{s : Set α} : ¬s.Infinite ↔ s.Finite

Full source

@[simp]
theorem not_infinite {s : Set α} : ¬s.Infinite¬s.Infinite ↔ s.Finite :=
  not_not

Equivalence of Non-Infinite and Finite Sets

Informal description

For any set $s$ over a type $\alpha$, the set $s$ is not infinite if and only if it is finite. In other words, $\neg (\text{Infinite}\ s) \leftrightarrow \text{Finite}\ s$.

Set.finite_or_infinite theorem

(s : Set α) : s.Finite ∨ s.Infinite

Full source

/-- See also `finite_or_infinite`, `fintypeOrInfinite`. -/
protected theorem finite_or_infinite (s : Set α) : s.Finite ∨ s.Infinite :=
  em _

Finite or Infinite Dichotomy for Sets

Informal description

For any set $s$ over a type $\alpha$, either $s$ is finite or $s$ is infinite.

Set.infinite_or_finite theorem

(s : Set α) : s.Infinite ∨ s.Finite

Full source

protected theorem infinite_or_finite (s : Set α) : s.Infinite ∨ s.Finite :=
  em' _

Dichotomy of Set Finiteness: Infinite or Finite

Informal description

For any set $s$ over a type $\alpha$, either $s$ is infinite or $s$ is finite.

Equiv.set_finite_iff theorem

{s : Set α} {t : Set β} (hst : s ≃ t) : s.Finite ↔ t.Finite

Full source

theorem Equiv.set_finite_iff {s : Set α} {t : Set β} (hst : s ≃ t) : s.Finite ↔ t.Finite := by
  simp_rw [← Set.finite_coe_iff, hst.finite_iff]

Finite Sets are Equivalent under Bijection

Informal description

Given sets $s \subseteq \alpha$ and $t \subseteq \beta$, and a bijection $h_{st} : s \simeq t$ between them, the set $s$ is finite if and only if $t$ is finite.

Set.infinite_coe_iff theorem

{s : Set α} : Infinite s ↔ s.Infinite

Full source

theorem infinite_coe_iff {s : Set α} : InfiniteInfinite s ↔ s.Infinite :=
  not_finite_iff_infinite.symm.trans finite_coe_iff.not

Equivalence of Infinite Type and Infinite Set for Subtypes

Informal description

For any set $s$ over a type $\alpha$, the type corresponding to $s$ (i.e., the subtype of elements in $s$) is infinite if and only if $s$ is an infinite set.