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.

source
@[protected, instance]
def option.fintype {α : Type u_1} [fintype α] :
fintype (option α)
Equations
source
theorem univ_option (α : Type u_1) [fintype α] :
finset.univ = ⇑finset.insert_none finset.univ
source
@[simp]
theorem fintype.card_option {α : Type u_1} [fintype α] :
fintype.card (option α) = fintype.card α + 1
source
def fintype_of_option {α : Type u_1} [fintype (option α)] :
fintype α

If option α is a fintype then so is α

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

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

Equations
source
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
source
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.

source
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.