Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-18 15:57 57bc1dab

View on Github →

feat(order/limsup_liminf, order/filter/ennreal): add properties of limsup for ennreal-valued functions (#5746)

Estimated changes

added theorem ae_lt_of_ess_sup_lt
added theorem ae_lt_of_lt_ess_inf
added theorem ennreal.ae_le_ess_sup
added theorem ennreal.ess_sup_add_le
added def ess_inf
added theorem ess_inf_congr_ae
added theorem ess_inf_const
added theorem ess_inf_const_top
added theorem ess_inf_measure_zero
added theorem ess_inf_mono_ae
added def ess_sup
added theorem ess_sup_congr_ae
added theorem ess_sup_const
added theorem ess_sup_const_bot
added theorem ess_sup_eq_zero_iff
added theorem ess_sup_measure_zero
added theorem ess_sup_mono_ae
added theorem ennreal.limsup_add_le
added theorem order_iso.liminf_apply
added theorem order_iso.limsup_apply