Documentation

Mathlib.Data.Fintype.Option

fintype instances for option #

instance instFintypeOption {α : Type u_3} [Fintype α] :
Equations
    @[simp]
    theorem Fintype.card_option {α : Type u_3} [Fintype α] :
    card (Option α) = card α + 1
    def fintypeOfOption {α : Type u_3} [Fintype (Option α)] :

    If Option α is a Fintype then so is α

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

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

        Equations
          Instances For
            def Fintype.truncRecEmptyOption {P : Type u → Sort v} (of_equiv : {α β : Type u} → α βP αP β) (h_empty : P PEmpty.{u + 1}) (h_option : {α : Type u} → [Fintype α] → [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
              Instances For
                theorem Fintype.induction_empty_option {P : (α : Type u) → [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} (a : α β), P αP β) (h_empty : P PEmpty.{u + 1}) (h_option : ∀ {α : Type u} [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.