Commit 2021-07-14 22:10 e343609b

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.