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

Equations

• Fintype.ofMultiset s H = { elems := s.toFinset, complete := ⋯ }

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

Construct a proof of Fintype α from a universal list

Equations

• Fintype.ofList l H = { elems := l.toFinset, complete := ⋯ }

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.

Equations

• Fintype.ofBijective f H = { elems := Finset.map { toFun := f, inj' := ⋯ } Finset.univ, complete := ⋯ }

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.

Equations

• Fintype.ofSurjective f H = { elems := Finset.image f Finset.univ, complete := ⋯ }

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.

Equations

• Fintype.ofInjective f H = if hα : Nonempty α then Fintype.ofSurjective (Function.invFun f) ⋯ else { elems := ∅, complete := ⋯ }

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

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

Equations

• Fintype.ofEquiv α f = Fintype.ofBijective ⇑f ⋯

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

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

Equations

• Fintype.ofSubsingleton a = { elems := {a}, complete := ⋯ }

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.

Equations

• Fintype.ofIsEmpty = { elems := ∅, complete := ⋯ }

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

Equations

• Fintype.instEmpty = Fintype.ofIsEmpty

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

Equations

• Fintype.instPEmpty = Fintype.ofIsEmpty