HepLean Documentation
Mathlib
.
Data
.
Finite
.
Powerset
Search
Google site search
return to top
source
Imports
Init
Mathlib.Data.Fintype.Powerset
Imported by
Finite
.
instSet
Finiteness of powersets
#
source
instance
Finite
.
instSet
{α :
Type
u_1}
[
Finite
α
]
:
Finite
(
Set
α
)
Equations
⋯
=
⋯