Documentation

Mathlib.MeasureTheory.Constructions.BorelSpace.Complex

Equip ℂ with the Borel sigma-algebra #

source
@[instance 900]
instance RCLike.measurableSpace {𝕜 : Type u_1} [RCLike 𝕜] :
MeasurableSpace 𝕜
Equations
    source
    @[instance 900]
    instance RCLike.borelSpace {𝕜 : Type u_1} [RCLike 𝕜] :
    BorelSpace 𝕜
    source
    instance Complex.measurableSpace :
    MeasurableSpace ℂ
    Equations
      source
      instance Complex.borelSpace :
      BorelSpace ℂ