Documentation

Mathlib.MeasureTheory.Constructions.BorelSpace.Complex

Equip with the Borel sigma-algebra #

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