mathlib3 documentation

data.finite.basic

Finite types #

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

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 #

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_locale 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

source
@[protected, instance]
def finite.of_subsingleton {α : Sort u_1} [subsingleton α] :
finite α
source
@[protected, nolint, instance]
def finite.prop (p : Prop) :
finite p
source
@[protected, instance]
def finite.prod.finite {α : Type u_1} {β : Type u_2} [finite α] [finite β] :
finite (α × β)
source
@[protected, instance]
def finite.pprod.finite {α : Sort u_1} {β : Sort u_2} [finite α] [finite β] :
finite (pprod α β)
source
theorem finite.prod_left {α : Type u_1} (β : Type u_2) [finite (α × β)] [nonempty β] :
finite α
source
theorem finite.prod_right {β : Type u_2} (α : Type u_1) [finite (α × β)] [nonempty α] :
finite β
source
@[protected, instance]
def finite.sum.finite {α : Type u_1} {β : Type u_2} [finite α] [finite β] :
finite (α ⊕ β)
source
theorem finite.sum_left {α : Type u_1} (β : Type u_2) [finite (α ⊕ β)] :
finite α
source
theorem finite.sum_right {β : Type u_2} (α : Type u_1) [finite (α ⊕ β)] :
finite β
source
@[protected, instance]
def finite.sigma.finite {α : Type u_1} {β : α → Type u_2} [finite α] [∀ (a : α), finite (β a)] :
finite (Σ (a : α), β a)
source
@[protected, instance]
def finite.psigma.finite {ι : Sort u_1} {π : ι → Sort u_2} [finite ι] [∀ (i : ι), finite (π i)] :
finite (Σ' (i : ι), π i)
source
@[protected, instance]
def finite.set.finite {α : Type u_1} [finite α] :
finite (set α)
source
@[protected, instance]
def subtype.finite {α : Sort u_1} [finite α] {p : α → Prop} :
finite {x // p x}

This instance also provides [finite s] for s : set α.

source
@[protected, instance]
def pi.finite {α : Sort u_1} {β : α → Sort u_2} [finite α] [∀ (a : α), finite (β a)] :
finite (Π (a : α), β a)
source
@[protected, instance]
def vector.finite {α : Type u_1} [finite α] {n : ℕ} :
finite (vector α n)
source
@[protected, instance]
def quot.finite {α : Sort u_1} [finite α] (r : α → α → Prop) :
finite (quot r)
source
@[protected, instance]
def quotient.finite {α : Sort u_1} [finite α] (s : setoid α) :
finite (quotient s)
source
@[protected, instance]
def function.embedding.finite {α : Sort u_1} {β : Sort u_2} [finite β] :
finite (α ↪ β)
source
@[protected, instance]
def equiv.finite_right {α : Sort u_1} {β : Sort u_2} [finite β] :
finite (α ≃ β)
source
@[protected, instance]
def equiv.finite_left {α : Sort u_1} {β : Sort u_2} [finite α] :
finite (α ≃ β)
source
@[protected, instance]
def sym.finite {α : Type u_1} [finite α] {n : ℕ} :
finite (sym α n)