Commit 2022-01-03 18:55 9d0fd523
View on Github →feat(measure_theory/function/lp_space): use has_measurable_add2 instead of second_countable_topology (#11202)
Use the weaker assumption [has_measurable_add₂ E] instead of [second_countable_topology E] in 4 lemmas.