Constructors for Fintype

This file contains basic constructors for Fintype instances, given maps from/to finite types.

Main results

• Fintype.ofBijective, Fintype.ofInjective, Fintype.ofSurjective: a type is finite if there is a bi/in/surjection from/to a finite type.

def Fintype.ofMultiset {α : Type u_1} [DecidableEq α] (s : Multiset α) (H : ∀ (x : α), x ∈ s) : Fintype α

Construct a proof of Fintype α from a universal multiset

def Fintype.ofList {α : Type u_1} [DecidableEq α] (l : List α) (H : ∀ (x : α), x ∈ l) : Fintype α

Construct a proof of Fintype α from a universal list

def Fintype.ofBijective {α : Type u_1} {β : Type u_2} [Fintype α] (f : α → β) (H : Function.Bijective f) : Fintype β

If f : α → β is a bijection and α is a fintype, then β is also a fintype.

def Fintype.ofSurjective {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] (f : α → β) (H : Function.Surjective f) : Fintype β

If f : α → β is a surjection and α is a fintype, then β is also a fintype.

noncomputable def Fintype.ofInjective {α : Type u_1} {β : Type u_2} [Fintype β] (f : α → β) (H : Function.Injective f) : Fintype α

Given an injective function to a fintype, the domain is also a fintype. This is noncomputable because injectivity alone cannot be used to construct preimages.

def Fintype.ofEquiv {β : Type u_2} (α : Type u_4) [Fintype α] (f : α ≃ β) : Fintype β

If f : α ≃ β and α is a fintype, then β is also a fintype.

def Fintype.ofSubsingleton {α : Type u_1} (a : α) [Subsingleton α] : Fintype α

Any subsingleton type with a witness is a fintype (with one term).

theorem Fintype.univ_ofSubsingleton {α : Type u_1} (a : α) [Subsingleton α] : Finset.univ = {a}

def Fintype.ofIsEmpty {α : Type u_1} [IsEmpty α] : Fintype α

An empty type is a fintype. Not registered as an instance, to make sure that there aren't two conflicting Fintype ι instances around when casing over whether a fintype ι is empty or not.

theorem Fintype.univ_ofIsEmpty {α : Type u_1} [IsEmpty α] : Finset.univ = ∅

Note: this lemma is specifically about Fintype.ofIsEmpty. For a statement about arbitrary Fintype instances, use Finset.univ_eq_empty.

instance Fintype.instEmpty : Fintype Empty

instance Fintype.instPEmpty : Fintype PEmpty.{u_4 + 1}