# fintype instances for option #

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

If Option α is a Fintype then so is α

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

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

Equations
• = fintypeOfOption
Instances For
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) [] [] :
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.
Instances For
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 : ) :

Internal induction hypothesis

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Fintype.induction_empty_option {P : (α : Type u) → [inst : ] → Prop} (of_equiv : ∀ (α β : Type u) [inst : ] (e : α β), P αP β) (h_empty : ) (h_option : ∀ (α : Type u) [inst : ], P αP ()) (α : Type u) [h_fintype : ] :
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.

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) [] :
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.