# Documentation

Mathlib.Data.Fintype.Option

# fintype instances for option #

instance instFintypeOption {α : Type u_1} [inst : ] :
Equations
• instFintypeOption = { elems := Finset.insertNone.toEmbedding Finset.univ, complete := (_ : ∀ (a : ), a Finset.insertNone.toEmbedding Finset.univ) }
theorem univ_option (α : Type u_1) [inst : ] :
Finset.univ = Finset.insertNone.toEmbedding Finset.univ
@[simp]
theorem Fintype.card_option {α : Type u_1} [inst : ] :
=
def fintypeOfOption {α : Type u_1} [inst : Fintype ()] :

If Option α is a Fintype then so is α

Equations
• fintypeOfOption = { elems := Finset.eraseNone Fintype.elems, complete := (_ : ∀ (x : α), x Finset.eraseNone Fintype.elems) }
def fintypeOfOptionEquiv {α : Type u_1} {β : Type u_2} [inst : ] (f : α ) :

A type is a Fintype if its successor (using Option) is a Fintype.

Equations
• = fintypeOfOption
def Fintype.truncRecEmptyOption {P : Type u → Sort v} (of_equiv : {α β : Type u} → α βP αP β) (h_empty : ) (h_option : {α : Type u} → [inst : ] → [inst : ] → P αP ()) (α : Type u) [inst : ] [inst : ] :
Trunc (P α)

A recursor principle for finite types, analogous to Nat.rec. It effectively says that every Fintype is either Empty or Option α, up to an Equiv.

Equations
• One or more equations did not get rendered due to their size.
def Fintype.truncRecEmptyOption.ind {P : Type u → Sort v} (of_equiv : {α β : Type u} → α βP αP β) (h_empty : ) (h_option : {α : Type u} → [inst : ] → [inst : ] → P αP ()) (n : ) :
Trunc (P (ULift (Fin n)))

Internal induction hypothesis

Equations
• One or more equations did not get rendered due to their size.
theorem Fintype.induction_empty_option {P : (α : Type u) → [inst : ] → Prop} (of_equiv : (α β : Type u) → [inst : ] → (e : α β) → P α ()P β inst) (h_empty : P PEmpty Fintype.ofIsEmpty) (h_option : (α : Type u) → [inst : ] → P α instP () instFintypeOption) (α : Type u) [h_fintype : ] :
P α h_fintype

An induction principle for finite types, analogous to Nat.rec. It effectively says that every Fintype is either Empty or Option α, up to an Equiv.

theorem Finite.induction_empty_option {P : Type u → Prop} (of_equiv : {α β : Type u} → α βP αP β) (h_empty : ) (h_option : {α : Type u} → [inst : ] → P αP ()) (α : Type u) [inst : ] :
P α

An induction principle for finite types, analogous to Nat.rec. It effectively says that every Fintype is either Empty or Option α, up to an Equiv.