fintype instances for option

instance instFintypeOption {α : Type u_3} [Fintype α] : Fintype (Option α)

Equations

• instFintypeOption = { elems := Finset.insertNone Finset.univ, complete := ⋯ }

theorem univ_option (α : Type u_3) [Fintype α] : Finset.univ = Finset.insertNone Finset.univ

@[simp]

theorem Fintype.card_option {α : Type u_3} [Fintype α] : Fintype.card (Option α) = Fintype.card α + 1

def fintypeOfOption {α : Type u_3} [Fintype (Option α)] : Fintype α

If Option α is a Fintype then so is α

Equations

• fintypeOfOption = { elems := Finset.eraseNone Fintype.elems, complete := ⋯ }

def fintypeOfOptionEquiv {α : Type u_1} {β : Type u_2} [Fintype α] (f : α ≃ Option β) : Fintype β

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

Equations

• fintypeOfOptionEquiv f = fintypeOfOption

def Fintype.truncRecEmptyOption {P : Type u → Sort v} (of_equiv : {α β : Type u} → α ≃ β → P α → P β) (h_empty : P PEmpty.{u + 1}) (h_option : {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)) (α : Type u) [Fintype α] [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.{u + 1}) (h_option : {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)) (n : ℕ) : Trunc (P (ULift.{u, 0} (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 α → P β) (h_empty : P PEmpty.{u + 1}) (h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)) (α : Type u) [h_fintype : 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 : P PEmpty.{u + 1}) (h_option : ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)) (α : Type u) [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.