Theorem measure_theory.mem_Lp_meas_to_Lp_of_trim
Modification history
2021-09-18 23:07
src/measure_theory/function/conditional_expectation.lean
feat(measure_theory/function/conditional_expectation): condexp_ind is ae_measurable' (#9263)
Deleted measure_theory.mem_Lp_meas_to_Lp_of_trimView on Github →