mathlib

ef78b322 - feat(measure_theory/function/lp_space): add lemmas about snorm and mem_Lp (#9146)

feat(measure_theory/function/lp_space): add lemmas about snorm and mem_Lp (#9146) Also move lemma `snorm_add_le` (and related others) out of the borel space section, since `opens_measurable_space` is a sufficient hypothesis.