Documentation
Mathlib
.
MeasureTheory
.
Constructions
.
BorelSpace
.
Complex
Search
Google site search
return to top
source
Imports
Init
Mathlib.Analysis.Complex.Basic
Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Imported by
RCLike
.
measurableSpace
RCLike
.
borelSpace
Complex
.
measurableSpace
Complex
.
borelSpace
Equip
ℂ
with the Borel sigma-algebra
#
source
@[instance 900]
instance
RCLike
.
measurableSpace
{𝕜 :
Type
u_1}
[
RCLike
𝕜
]
:
MeasurableSpace
𝕜
Equations
RCLike.measurableSpace
=
borel
𝕜
source
@[instance 900]
instance
RCLike
.
borelSpace
{𝕜 :
Type
u_1}
[
RCLike
𝕜
]
:
BorelSpace
𝕜
source
instance
Complex
.
measurableSpace
:
MeasurableSpace
ℂ
Equations
Complex.measurableSpace
=
borel
ℂ
source
instance
Complex
.
borelSpace
:
BorelSpace
ℂ