Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-13 22:32 30045133

View on Github →

feat(measure_theory/ess_sup): monotonicity of ess_sup/ess_inf w.r.t. the measure (#7917)

Estimated changes

Modified src/measure_theory/ess_sup.lean

modified theorem ennreal.ess_sup_const_mul

modified theorem ennreal.ess_sup_eq_zero_iff

added theorem ess_inf_antimono_measure

added theorem ess_sup_le_of_ae_le

added theorem ess_sup_mono_measure

added theorem le_ess_inf_of_ae_le

Modified src/order/liminf_limsup.lean

added theorem filter.liminf_le_liminf_of_le

added theorem filter.limsup_le_limsup_of_le