Documentation

Mathlib.Data.Fintype.Option

fintype instances for option #

instance instFintypeOption {α : Type u_4} [Fintype α] :
Equations
  • instFintypeOption = { elems := Finset.insertNone Finset.univ, complete := (_ : ∀ (a : Option α), a Finset.insertNone Finset.univ) }
theorem univ_option (α : Type u_4) [Fintype α] :
Finset.univ = Finset.insertNone Finset.univ
@[simp]
theorem Fintype.card_option {α : Type u_4} [Fintype α] :
def fintypeOfOption {α : Type u_4} [Fintype (Option α)] :

If Option α is a Fintype then so is α

Equations
  • fintypeOfOption = { elems := Finset.eraseNone Fintype.elems, complete := (_ : ∀ (x : α), x Finset.eraseNone Fintype.elems) }
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} → [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.
      Instances For
        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 : ) :

        Internal induction hypothesis

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem Fintype.induction_empty_option {P : (α : Type u) → [inst : Fintype α] → Prop} (of_equiv : (α β : Type u) → [inst : Fintype β] → (e : α β) → P α (Fintype.ofEquiv β e.symm)P β inst) (h_empty : P PEmpty.{u + 1} Fintype.ofIsEmpty) (h_option : (α : Type u) → [inst : Fintype α] → P α instP (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.

          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.