mathlib

f0713cb9 - refactor(measure_theory/simple_func_dense): split monolithic proof (#4199)

refactor(measure_theory/simple_func_dense): split monolithic proof (#4199) In the new proof the sequence of approximating functions has a simpler description: `N`-th function sends `x` to the point `e k` which is the nearest to `f x` among the points `e 0`, ..., `e N`, where `e n` is a dense sequence such that `e 0 = 0`.