Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-26 20:25 27791f97

View on Github →

feat(data/real/nnreal): add mul csupr/cinfi lemmas (#13936)

Estimated changes

Modified src/algebra/order/with_zero.lean

added theorem div_le_div_left₀

added theorem mul_le_mul_left₀

added def order_iso.mul_left₀'

added theorem order_iso.mul_left₀'_symm

added def order_iso.mul_right₀'

added theorem order_iso.mul_right₀'_symm

Modified src/data/real/basic.lean

added theorem real.infi_of_not_bdd_below

added theorem real.supr_of_not_bdd_above

Modified src/data/real/nnreal.lean

added theorem nnreal.Sup_of_not_bdd_above

added theorem nnreal.infi_const_zero

added theorem nnreal.infi_empty

added theorem nnreal.infi_mul

added theorem nnreal.le_infi_mul

added theorem nnreal.le_infi_mul_infi

added theorem nnreal.le_mul_infi

added theorem nnreal.le_to_nnreal_of_coe_le

added theorem nnreal.mul_infi

added theorem nnreal.mul_supr

added theorem nnreal.mul_supr_le

added theorem nnreal.supr_div

added theorem nnreal.supr_mul

added theorem nnreal.supr_mul_le

added theorem nnreal.supr_mul_supr_le

added theorem nnreal.supr_of_not_bdd_above

Modified src/data/set/pointwise.lean

added theorem set.inv_range

added theorem set.smul_set_range