Documentation
Mathlib
.
Data
.
Fintype
.
WithTopBot
Search
return to top
source
Imports
Init
Mathlib.Order.TypeTags
Mathlib.Data.Fintype.Option
Imported by
instFintypeWithTop
instFiniteWithTop
instFintypeWithBot
instFiniteWithBot
Fintype instances for
WithTop
α
and
WithBot
α
#
source
instance
instFintypeWithTop
{
α
:
Type
u_1}
[
Fintype
α
]
:
Fintype
(
WithTop
α
)
Equations
instFintypeWithTop
=
instFintypeOption
source
instance
instFiniteWithTop
{
α
:
Type
u_1}
[
Finite
α
]
:
Finite
(
WithTop
α
)
source
instance
instFintypeWithBot
{
α
:
Type
u_1}
[
Fintype
α
]
:
Fintype
(
WithBot
α
)
Equations
instFintypeWithBot
=
instFintypeOption
source
instance
instFiniteWithBot
{
α
:
Type
u_1}
[
Finite
α
]
:
Finite
(
WithBot
α
)