Commit 2024-07-16 05:50 60750e14

feat(Measure/WithDensity): drop measurability assumption (#14736)

• Show that for an s-finite measure, any function is equivalent to a measurable function in the sense of Lebesgue integrals over subsets.
• Use it to drop measurability assumption and add an instance Measure.withDensity.instSFinite.