Documentation

Mathlib.MeasureTheory.Constructions.BorelSpace.Complex

Equip with the Borel sigma-algebra #

@[instance 900]
instance RCLike.measurableSpace {𝕜 : Type u_1} [RCLike 𝕜] :
Equations
  • RCLike.measurableSpace = borel 𝕜
@[instance 900]
instance RCLike.borelSpace {𝕜 : Type u_1} [RCLike 𝕜] :
Equations
  • =