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

class inductive 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

  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.

• intro {α : Sort u_3} {n : ℕ} : α ≃ Fin n → Finite α

theorem finite_iff_exists_equiv_fin {α : Sort u_3} : Finite α ↔ ∃ (n : ℕ), Nonempty (α ≃ Fin n)

theorem Finite.exists_equiv_fin (α : Sort u_3) [h : Finite α] : ∃ (n : ℕ), Nonempty (α ≃ Fin n)

theorem Finite.of_equiv {β : Sort u_2} (α : Sort u_3) [h : Finite α] (f : α ≃ β) : Finite β

theorem Equiv.finite_iff {α : Sort u_1} {β : Sort u_2} (f : α ≃ β) : Finite α ↔ Finite β

theorem Function.Bijective.finite_iff {α : Sort u_1} {β : Sort u_2} {f : α → β} (h : Function.Bijective f) : Finite α ↔ Finite β

theorem Finite.ofBijective {α : Sort u_1} {β : Sort u_2} [Finite α] {f : α → β} (h : Function.Bijective f) : Finite β

theorem Finite.nonempty_decidableEq (α : Sort u_1) [Finite α] : Nonempty (DecidableEq α)

instance instFinitePLift {α : Sort u_1} [Finite α] : Finite (PLift α)

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

class Infinite (α : Sort u_3) : Prop

A type is said to be infinite if it is not finite. Note that Infinite α is equivalent to IsEmpty (Fintype α) or IsEmpty (Finite α).

• not_finite : ¬Finite α

  assertion that α is ¬Finite

@[simp]

theorem not_finite_iff_infinite {α : Sort u_1} : ¬Finite α ↔ Infinite α

@[simp]

theorem not_infinite_iff_finite {α : Sort u_1} : ¬Infinite α ↔ Finite α

theorem Equiv.infinite_iff {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) : Infinite α ↔ Infinite β

instance instInfinitePLift {α : Sort u_1} [Infinite α] : Infinite (PLift α)

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

theorem finite_or_infinite (α : Sort u_3) : Finite α ∨ Infinite α

theorem not_finite (α : Sort u_3) [Infinite α] [Finite α] : False

Infinite α is not Finite

theorem Finite.false {α : Sort u_1} [Infinite α] : Finite α → False

theorem Infinite.false {α : Sort u_1} [Finite α] : Infinite α → False

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.

instance Bool.instFinite : Finite Bool

instance Prop.instFinite : Finite Prop

Finite sets

def Set.Finite {α : Type u} (s : Set α) : Prop

A set is finite if the corresponding Subtype is finite, i.e., if there exists a natural n : ℕ and an equivalence s ≃ Fin n.

Equations

• s.Finite = Finite ↑s

theorem Set.finite_coe_iff {α : Type u} {s : Set α} : Finite ↑s ↔ s.Finite

theorem Set.toFinite {α : Type u} (s : Set α) [Finite ↑s] : s.Finite

Constructor for Set.Finite using a Finite instance.

theorem Set.Finite.to_subtype {α : Type u} {s : Set α} (h : s.Finite) : Finite ↑s

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.

def Set.Infinite {α : Type u} (s : Set α) : Prop

A set is infinite if it is not finite.

This is protected so that it does not conflict with global Infinite.

Equations

• s.Infinite = ¬s.Finite

@[simp]

theorem Set.not_infinite {α : Type u} {s : Set α} : ¬s.Infinite ↔ s.Finite

@[simp]

theorem Set.Finite.not_infinite {α : Type u} {s : Set α} : s.Finite → ¬s.Infinite

Alias of the reverse direction of Set.not_infinite.

theorem Set.finite_or_infinite {α : Type u} (s : Set α) : s.Finite ∨ s.Infinite

See also finite_or_infinite, fintypeOrInfinite.

theorem Set.infinite_or_finite {α : Type u} (s : Set α) : s.Infinite ∨ s.Finite

theorem Equiv.set_finite_iff {α : Type u} {β : Type v} {s : Set α} {t : Set β} (hst : ↑s ≃ ↑t) : s.Finite ↔ t.Finite

Infinite sets

theorem Set.infinite_coe_iff {α : Type u} {s : Set α} : Infinite ↑s ↔ s.Infinite

theorem Set.Infinite.to_subtype {α : Type u} {s : Set α} : s.Infinite → Infinite ↑s

Alias of the reverse direction of Set.infinite_coe_iff.