Documentation

Mathlib.Data.Fintype.Option

fintype instances for option #

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

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 : Fintype α] (f : α Option β) :

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

Equations
def Fintype.truncRecEmptyOption {P : Type u → Sort v} (of_equiv : {α β : Type u} → α βP αP β) (h_empty : P PEmpty) (h_option : {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P αP (Option α)) (α : Type u) [inst : Fintype α] [inst : DecidableEq α] :
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 : P PEmpty) (h_option : {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P αP (Option α)) (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 : Fintype α] → Prop} (of_equiv : (α β : Type u) → [inst : Fintype β] → (e : α β) → P α (Fintype.ofEquiv β (Equiv.symm e))P β inst) (h_empty : P PEmpty Fintype.ofIsEmpty) (h_option : (α : Type u) → [inst : Fintype α] → P α instP (Option α) instFintypeOption) (α : Type u) [h_fintype : 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 : P PEmpty) (h_option : {α : Type u} → [inst : Fintype α] → P αP (Option α)) (α : Type u) [inst : Finite α] :
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.