Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-19 18:42 9d14a5f3

View on Github →

chore(order/filter/basic): add eventually_eq.rfl and eventually_le.rfl (#5805)

Estimated changes

Modified src/analysis/asymptotic_equivalent.lean

Modified src/measure_theory/interval_integral.lean

Modified src/measure_theory/measure_space.lean

modified theorem measure_theory.ae_eq_refl

Modified src/order/filter/basic.lean

added theorem filter.eventually_eq.rfl

added theorem filter.eventually_le.rfl

Modified src/order/liminf_limsup.lean