mathlib

9d0fd523 - feat(measure_theory/function/lp_space): use has_measurable_add2 instead of second_countable_topology (#11202)

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.