Documentation
MDP
.
ENNRealExt
Search
return to top
source
Imports
Init
Mathlib.Topology.Instances.ENNReal.Lemmas
Imported by
ENNReal
.
tsum_biUnion'
ENNReal
.
tsum_biUnion
Extensions to
ENNReal
#
The intention is to upstream these to mathlib.
source
theorem
ENNReal
.
tsum_biUnion'
{
α
:
Type
u_2}
{
ι
:
Type
u_1}
{
S
:
Set
ι
}
{
f
:
α
→
ENNReal
}
{
t
:
ι
→
Set
α
}
(
h
:
S
.
PairwiseDisjoint
t
)
:
∑'
(
x
:
↑
(⋃
i
∈
S
,
t
i
)
)
,
f
↑
x
=
∑'
(
i
:
↑
S
) (
x
:
↑
(
t
↑
i
)
)
,
f
↑
x
source
theorem
ENNReal
.
tsum_biUnion
{
α
:
Type
u_2}
{
ι
:
Type
u_1}
{
f
:
α
→
ENNReal
}
{
t
:
ι
→
Set
α
}
(
h
:
Set.univ
.
PairwiseDisjoint
t
)
:
∑'
(
x
:
↑
(⋃ (
i
:
ι
),
t
i
)
)
,
f
↑
x
=
∑'
(
i
:
ι
) (
x
:
↑
(
t
i
)
)
,
f
↑
x