mathlib3 documentation

data.fintype.option

fintype instances for option #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[protected, instance]
def option.fintype {α : Type u_1} [fintype α] :
Equations
@[simp]
theorem fintype.card_option {α : Type u_1} [fintype α] :
def fintype_of_option {α : Type u_1} [fintype (option α)] :

If option α is a fintype then so is α

Equations
def fintype_of_option_equiv {α : Type u_1} {β : Type u_2} [fintype α] (f : α option β) :

A type is a fintype if its successor (using option) is a fintype.

Equations
def fintype.trunc_rec_empty_option {P : Type u Sort v} (of_equiv : Π {α β : Type u}, α β P α P β) (h_empty : P pempty) (h_option : Π {α : Type u} [_inst_1 : fintype α] [_inst_2 : decidable_eq α], P α P (option α)) (α : Type u) [fintype α] [decidable_eq α] :
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
theorem fintype.induction_empty_option {P : Π (α : Type u) [_inst_1 : fintype α], Prop} (of_equiv : (α β : Type u) [_inst_2 : fintype β] (e : α β), P α P β) (h_empty : P pempty) (h_option : (α : Type u) [_inst_3 : fintype α], P α P (option α)) (α : Type u) [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) (h_option : {α : Type u} [_inst_1 : 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.