Commit 2024-09-19 20:54 f0308a5a

feat: separable measure and sufficient condition for Lp spaces to be second-countable (#12519) Define the notion of measure-dense family in a measure space, and the notion of separable measure. Prove that if a measure is separable and E is a second-countable NormedAddCommGroup, then the corresponding Lp space is second-countable. True in particular when the measurable space is countably generated and the measure is s-finite.