Documentation

Mathlib.Data.Fintype.WithTopBot

Fintype instances for WithTop α and WithBot α #

source
🔸 coverage
instance instFintypeWithTop {α : Type u_1} [Fintype α] :
Fintype (WithTop α)
Equations
    source
    📐 coverage
    instance instFiniteWithTop {α : Type u_1} [Finite α] :
    Finite (WithTop α)
    source
    🔸 coverage
    instance instFintypeWithBot {α : Type u_1} [Fintype α] :
    Fintype (WithBot α)
    Equations
      source
      📐 coverage
      instance instFiniteWithBot {α : Type u_1} [Finite α] :
      Finite (WithBot α)