Equip ℂ with the Borel sigma-algebra

@[instance 900]

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

Equations

• RCLike.measurableSpace = borel 𝕜

@[instance 900]

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

Equations

• ⋯ = ⋯

instance Complex.measurableSpace : MeasurableSpace ℂ

Equations

• Complex.measurableSpace = borel ℂ

instance Complex.borelSpace : BorelSpace ℂ

Equations

• Complex.borelSpace = ⋯