fintype instances for option #

source

ink

instance instFintypeOption {α : Type u_1} [inst : Fintype α] :

Fintype (Option α)

Equations

instFintypeOption = { elems := ↑Finset.insertNone.toEmbedding Finset.univ, complete := (_ : ∀ (a : Option α), a ∈ ↑Finset.insertNone.toEmbedding Finset.univ) }

source

ink

theorem univ_option (α : Type u_1) [inst : Fintype α] :

Finset.univ = ↑Finset.insertNone.toEmbedding Finset.univ

source

ink

@[simp]

theorem Fintype.card_option {α : Type u_1} [inst : Fintype α] :

Fintype.card (Option α) = Fintype.card α + 1

source

ink

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

Fintype α

If Option α is a Fintype then so is α

Equations

fintypeOfOption = { elems := ↑Finset.eraseNone Fintype.elems, complete := (_ : ∀ (x : α), x ∈ ↑Finset.eraseNone Fintype.elems) }

source

ink

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

Fintype β

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

Equations

fintypeOfOptionEquiv f = fintypeOfOption

source

ink

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.

source

ink

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.

source

ink

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 α inst → P (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.

source

ink

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.