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.

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