mathlib3
7c4f395a - feat(measure_theory): add `is_R_or_C.measurable_space` (#10417)

Commit

4 years ago

feat(measure_theory): add `is_R_or_C.measurable_space` (#10417) Don't remove specific instances because otherwise Lean fails to generate `borel_space (ι → ℝ)`.

Author

urkud

Parents

a1338d62

mathlib3 7c4f395a - feat(measure_theory): add `is_R_or_C.measurable_space` (#10417)

mathlib3
7c4f395a - feat(measure_theory): add `is_R_or_C.measurable_space` (#10417)