Documentation
PFR
.
Mathlib
.
MeasureTheory
.
Integral
.
SetIntegral
Search
return to top
source
Imports
Init
Mathlib.MeasureTheory.Integral.SetIntegral
Imported by
MeasureTheory
.
integral_eq_setIntegral
source
theorem
MeasureTheory
.
integral_eq_setIntegral
{
α
:
Type
u_1}
{
E
:
Type
u_2}
[
MeasurableSpace
α
]
[
NormedAddCommGroup
E
]
[
NormedSpace
ℝ
E
]
{
μ
:
Measure
α
}
{
s
:
Set
α
}
(
hs
:
μ
s
ᶜ
=
0
)
(
f
:
α
→
E
)
:
∫
(
x
:
α
)
,
f
x
∂
μ
=
∫
(
x
:
α
)
in
s
,
f
x
∂
μ