Documentation
Carleson
.
ToMathlib
.
Data
.
Set
.
Finite
.
Lattice
Search
return to top
source
Imports
Init
Mathlib.Data.Set.Finite.Lattice
Imported by
Set
.
finite_biUnion_iff_of_pairwiseDisjoint
Set
.
finite_iUnion_iff_of_pairwiseDisjoint
source
theorem
Set
.
finite_biUnion_iff_of_pairwiseDisjoint
{ι :
Type
u_1}
{α :
Type
u_2}
{f :
ι
→
Set
α
}
{s :
Set
ι
}
(hs :
s
.PairwiseDisjoint
f
)
:
(⋃
i
∈
s
,
f
i
)
.Finite
↔
(∀
i
∈
s
,
(
f
i
)
.Finite
)
∧
{
i
:
ι
|
i
∈
s
∧
(
f
i
)
.Nonempty
}
.Finite
source
theorem
Set
.
finite_iUnion_iff_of_pairwiseDisjoint
{ι :
Type
u_1}
{α :
Type
u_2}
{f :
ι
→
Set
α
}
(hs :
Set.univ
.PairwiseDisjoint
f
)
:
(⋃ (
i
:
ι
),
f
i
)
.Finite
↔
(∀ (
i
:
ι
),
(
f
i
)
.Finite
)
∧
{
i
:
ι
|
(
f
i
)
.Nonempty
}
.Finite