Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-24 10:39 f0713cb9

View on Github →

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.

Estimated changes

added theorem nat.range_cases_on
added theorem nat.range_of_succ
added theorem nat.range_rec
modified theorem set.sep_set_of
added theorem set.set_of_and
added theorem set.set_of_or
added theorem is_measurable_lt'
added theorem is_measurable_lt
modified theorem measurable.const_mul
modified theorem measurable.const_smul
modified theorem measurable.mul_const
added theorem measurable_edist_left
added theorem measurable_edist_right
modified theorem measure_theory.ae_eq_bot