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

• @IsROrC.borelSpace = @IsROrC.borelSpace.proof_1

instance Complex.measurableSpace : MeasurableSpace ℂ

Equations

• Complex.measurableSpace = borel ℂ

instance Complex.borelSpace : BorelSpace ℂ

Equations

• Complex.borelSpace = Complex.borelSpace.proof_1