mathlib

e343609b - feat(measure_theory/simple_func_dense): induction lemmas for Lp.simple_func and Lp (#8300)

feat(measure_theory/simple_func_dense): induction lemmas for Lp.simple_func and Lp (#8300) The new lemmas, `Lp.simple_func.induction`, `Lp.induction`, allow one to prove a predicate for all elements of `Lp.simple_func` / `Lp` (here p < ∞), by proving it for characteristic functions and then checking it behaves appropriately under addition, and, in the second case, taking limits. They are modelled on existing lemmas such as `simple_func.induction`, `mem_ℒp.induction`, `integrable.induction`.