mathlib3 documentation

measure_theory.constructions.borel_space.complex

Equip ℂ with the Borel sigma-algebra #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
@[protected, instance]
def is_R_or_C.measurable_space {𝕜 : Type u_1} [is_R_or_C 𝕜] :
measurable_space 𝕜
Equations
source
@[protected, instance]
def is_R_or_C.borel_space {𝕜 : Type u_1} [is_R_or_C 𝕜] :
borel_space 𝕜
source
@[protected, instance]
noncomputable def complex.measurable_space  :
measurable_space ℂ
Equations
source
@[protected, instance]
def complex.borel_space  :
borel_space ℂ