Documentation
PFR
.
Mathlib
.
MeasureTheory
.
Measure
.
MeasureSpaceDef
Search
return to top
source
Imports
Init
Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Imported by
MeasureTheory
.
measure_eq_univ_of_forall_singleton
source
theorem
MeasureTheory
.
measure_eq_univ_of_forall_singleton
{
Ω
:
Type
u_1}
[
Countable
Ω
]
[
MeasurableSpace
Ω
]
{
μ
:
Measure
Ω
}
{
s
:
Set
Ω
}
(
hμ
:
∀
x
∈
s
ᶜ
,
μ
{
x
}
=
0
)
:
μ
s
=
μ
Set.univ