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.

source

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 := ⋯ }

source

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 := ⋯ }

source

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 := ⋯ }

source

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 := ⋯ }

source

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 := ⋯ }

source

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 ⋯

source

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 := ⋯ }

source

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

Finset.univ = {a}

source

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