Documentation
Mathlib
.
Data
.
Fintype
.
Sigma
Search
Google site search
Mathlib
.
Data
.
Fintype
.
Sigma
source
Imports
Init
Mathlib.Data.Finset.Sigma
Mathlib.Data.Fintype.Basic
Imported by
instFintypeSigma
Finset
.
univ_sigma_univ
PSigma
.
fintype
fintype instances for sigma types
#
source
instance
instFintypeSigma
{α :
Type
u_4}
(β :
α
→
Type
u_5
)
[
Fintype
α
]
[
(
a
:
α
) →
Fintype
(
β
a
)
]
:
Fintype
(
Sigma
β
)
source
@[simp]
theorem
Finset
.
univ_sigma_univ
{α :
Type
u_4}
{β :
α
→
Type
u_5
}
[
Fintype
α
]
[
(
a
:
α
) →
Fintype
(
β
a
)
]
:
(
Finset.sigma
Finset.univ
fun
a
=>
Finset.univ
)
=
Finset.univ
source
instance
PSigma
.
fintype
{α :
Type
u_4}
{β :
α
→
Type
u_5
}
[
Fintype
α
]
[
(
a
:
α
) →
Fintype
(
β
a
)
]
:
Fintype
(
(a :
α
) ×'
β
a
)