Documentation
MeanFourier
.
Mathlib
.
Data
.
Fintype
.
Pi
Search
return to top
source
Imports
Init
Mathlib.Data.Fintype.Pi
MeanFourier.Mathlib.Data.Finset.Pi
Imported by
Set
.
Finite
.
univ_pi
source
theorem
Set
.
Finite
.
univ_pi
{
ι
:
Type
u_1}
{
α
:
ι
→
Type
u_2
}
{
t
:
(
i
:
ι
) →
Set
(
α
i
)
}
(
ht
:
∀ (
i
:
ι
),
(
t
i
)
.
Finite
)
(
ht'
:
{
i
:
ι
|
(
t
i
)
.
Nontrivial
}
.
Finite
)
:
(
univ
.
pi
t
)
.
Finite