Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-23 16:49 7c4f395a

View on Github →

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

Estimated changes

Modified src/measure_theory/constructions/borel_space.lean

Modified src/measure_theory/function/conditional_expectation.lean

modified theorem measure_theory.ae_measurable'.const_inner

modified theorem measure_theory.norm_condexp_L2_le_one

Modified src/measure_theory/function/l1_space.lean

modified theorem measure_theory.integrable.of_real

modified theorem measure_theory.integrable.re_im_iff

Modified src/measure_theory/function/l2_space.lean

Modified src/measure_theory/function/lp_space.lean

Modified src/measure_theory/function/special_functions.lean

Modified src/measure_theory/integral/set_integral.lean

modified theorem continuous_linear_map.continuous_integral_comp_L1

modified def measure_theory.Lp_to_Lp_restrict_clm

modified theorem measure_theory.Lp_to_Lp_restrict_clm_coe_fn

modified theorem measure_theory.Lp_to_Lp_restrict_smul