Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-02 08:57 f59f5d55

View on Github →

feat(data/real/ennreal): minor additions to ennreal (#558)

Estimated changes

Modified analysis/ennreal.lean

Modified analysis/metric_space.lean

Modified data/real/ennreal.lean

added theorem ennreal.add_lt_add_iff_right

added theorem ennreal.add_lt_top

added theorem ennreal.bit0_eq_top_iff

added theorem ennreal.bit0_eq_zero_iff

added theorem ennreal.bit0_inj

added theorem ennreal.bit1_eq_one_iff

added theorem ennreal.bit1_eq_top_iff

added theorem ennreal.bit1_inj

added theorem ennreal.bit1_ne_zero

added theorem ennreal.coe_bit0

added theorem ennreal.coe_bit1

modified theorem ennreal.coe_div

added theorem ennreal.coe_inv

modified theorem ennreal.div_le_iff_le_mul

modified theorem ennreal.div_pos_iff

added theorem ennreal.div_zero_iff

added theorem ennreal.exists_inv_nat_lt

added theorem ennreal.half_lt_self

added theorem ennreal.half_pos

deleted theorem ennreal.inv_coe

modified theorem ennreal.inv_eq_top

modified theorem ennreal.inv_eq_zero

modified theorem ennreal.inv_inv

modified theorem ennreal.inv_ne_top

modified theorem ennreal.inv_ne_zero

added theorem ennreal.mul_eq_top

added theorem ennreal.mul_eq_zero

added theorem ennreal.sub_eq_zero_iff_le

added theorem ennreal.zero_lt_sub_iff_lt

Modified data/real/nnreal.lean

modified theorem nnreal.add_halves

added theorem nnreal.half_lt_self

modified theorem nnreal.of_real_le_of_real_iff

added theorem nnreal.of_real_lt_of_real_iff