Documentation

Mathlib.Data.Finite.Basic

Finite types #

In this file we prove some theorems about Finite and provide some instances. This typeclass is a Prop-valued counterpart of the typeclass Fintype. See more details in the file where Finite is defined.

Main definitions #

Fintype.finite, Finite.of_fintype creates a Finite instance from a Fintype instance. The former lemma takes Fintype α as an explicit argument while the latter takes it as an instance argument.
Fintype.of_finite noncomputably creates a Fintype instance from a Finite instance.

Implementation notes #

There is an apparent duplication of many Fintype instances in this module, however they follow a pattern: if a Fintype instance depends on Decidable instances or other Fintype instances, then we need to "lower" the instance to be a Finite instance by removing the decidable instances and switching the Fintype instances to Finite instances. These are precisely the ones that cannot be inferred using Finite.of_fintype. (However, when using open Classical or the classical tactic the instances relying only on Decidable instances will give Finite instances.) In the future we might consider writing automation to create these "lowered" instances.

Tags #

finiteness, finite types

instance Finite.of_subsingleton {α : Sort u_1} [inst : Subsingleton α] :

Equations

@Finite.of_subsingleton = @Finite.of_subsingleton.proof_1

instance Finite.prop (p : Prop) :

Equations

Finite.prop = Finite.prop.proof_1

instance Finite.instFiniteProd {α : Type u_1} {β : Type u_2} [inst : Finite α] [inst : Finite β] :

Finite (α × β)

Equations

@Finite.instFiniteProd = @Finite.instFiniteProd.proof_1

instance Finite.instFinitePProd {α : Sort u_1} {β : Sort u_2} [inst : Finite α] [inst : Finite β] :

Finite (PProd α β)

Equations

@Finite.instFinitePProd = @Finite.instFinitePProd.proof_1

theorem Finite.prod_left {α : Type u_2} (β : Type u_1) [inst : Finite (α × β)] [inst : Nonempty β] :

theorem Finite.prod_right {β : Type u_2} (α : Type u_1) [inst : Finite (α × β)] [inst : Nonempty α] :

instance Finite.instFiniteSum {α : Type u_1} {β : Type u_2} [inst : Finite α] [inst : Finite β] :

Finite (α ⊕ β)

Equations

@Finite.instFiniteSum = @Finite.instFiniteSum.proof_1

theorem Finite.sum_left {α : Type u_2} (β : Type u_1) [inst : Finite (α ⊕ β)] :

theorem Finite.sum_right {β : Type u_2} (α : Type u_1) [inst : Finite (α ⊕ β)] :

instance Finite.instFiniteSigma {α : Type u_1} {β : α → Type u_2} [inst : Finite α] [inst : ∀ (a : α), Finite (β a)] :

Finite ((a : α) × β a)

Equations

@Finite.instFiniteSigma = @Finite.instFiniteSigma.proof_1

instance Finite.instFinitePSigma {ι : Sort u_1} {π : ι → Sort u_2} [inst : Finite ι] [inst : ∀ (i : ι), Finite (π i)] :

Finite ((i : ι) ×' π i)

Equations

@Finite.instFinitePSigma = @Finite.instFinitePSigma.proof_1

instance Finite.instFiniteSet {α : Type u_1} [inst : Finite α] :

Finite (Set α)

Equations

@Finite.instFiniteSet = @Finite.instFiniteSet.proof_1

instance Subtype.finite {α : Sort u_1} [inst : Finite α] {p : α → Prop} :

Finite { x // p x }

This instance also provides [Finite s] for s : Set α.

Equations

@Subtype.finite = @Subtype.finite.proof_1

instance Pi.finite {α : Sort u_1} {β : α → Sort u_2} [inst : Finite α] [inst : ∀ (a : α), Finite (β a)] :

Finite ((a : α) → β a)

Equations

@Pi.finite = @Pi.finite.proof_1

instance Vector.finite {α : Type u_1} [inst : Finite α] {n : ℕ} :

Finite (Vector α n)

Equations

@Vector.finite = @Vector.finite.proof_1

instance Quot.finite {α : Sort u_1} [inst : Finite α] (r : α → α → Prop) :

Finite (Quot r)

Equations

@Quot.finite = @Quot.finite.proof_1

instance Quotient.finite {α : Sort u_1} [inst : Finite α] (s : Setoid α) :

Finite (Quotient s)

Equations

@Quotient.finite = @Quotient.finite.proof_1

instance Function.Embedding.finite {α : Sort u_1} {β : Sort u_2} [inst : Finite β] :

Finite (α ↪ β)

Equations

@Function.Embedding.finite = @Function.Embedding.finite.proof_1

instance Equiv.finite_right {α : Sort u_1} {β : Sort u_2} [inst : Finite β] :

Finite (α ≃ β)

Equations

@Equiv.finite_right = @Equiv.finite_right.proof_1

instance Equiv.finite_left {α : Sort u_1} {β : Sort u_2} [inst : Finite α] :

Finite (α ≃ β)

Equations

@Equiv.finite_left = @Equiv.finite_left.proof_1

instance instFiniteSym {α : Type u_1} [inst : Finite α] {n : ℕ} :

Finite (Sym α n)

Equations

@instFiniteSym = @instFiniteSym.proof_1