Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-03 10:04 61db67de

View on Github →

chore(measure_theory/integration): define composition of a simple_func and a measurable function (#3667)

Estimated changes