Equip ℂ with the Borel sigma-algebra

instance IsROrC.measurableSpace {𝕜 : Type u_1} [IsROrC 𝕜] : MeasurableSpace 𝕜

Equations

• IsROrC.measurableSpace = borel 𝕜

instance IsROrC.borelSpace {𝕜 : Type u_1} [IsROrC 𝕜] : BorelSpace 𝕜

Equations

• (_ : BorelSpace 𝕜) = (_ : BorelSpace 𝕜)

instance Complex.measurableSpace : MeasurableSpace ℂ

Equations

• Complex.measurableSpace = borel ℂ

instance Complex.borelSpace : BorelSpace ℂ

Equations

• Complex.borelSpace = (_ : BorelSpace ℂ)