Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-02 16:08 fa7fdcae

View on Github →

feat(measure_theory/function/ae_eq_of_integral): two ennreal-valued function are a.e. equal if their integrals agree (#9372)

Estimated changes

Modified src/measure_theory/function/ae_eq_of_integral.lean

added theorem measure_theory.ae_measurable.ae_eq_of_forall_set_lintegral_eq

Modified src/order/filter/basic.lean

added theorem filter.eventually.lt_top_iff_ne_top

added theorem filter.eventually.lt_top_of_ne

added theorem filter.eventually.ne_of_lt

added theorem filter.eventually.ne_top_of_lt

Modified src/topology/instances/ennreal.lean

added theorem ennreal.eventually_eq_of_to_real_eventually_eq