mathlib

10ebb718 - feat(measure_theory): induction principles in measure theory (#3978)

feat(measure_theory): induction principles in measure theory (#3978) This commit adds three induction principles for measure theory * To prove something for arbitrary simple functions * To prove something for arbitrary measurable functions into `ennreal` * To prove something for arbitrary measurable + integrable functions. This also adds some basic lemmas to various files. Not all of them are used in this PR, some will be used by near-future PRs. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>