Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-05 08:48 83eda07e

View on Github →

refactor(data/real/ennreal): golf, generalize (#14996)

Add new lemmas

  • ennreal.bit0_strict_mono, ennreal.bit0_injective, ennreal.bit0_lt_bit0, ennreal.bit0_le_bit0, ennreal.bit0_top;
  • ennreal.bit1_strict_mono, ennreal.bit1_injective, ennreal.bit1_lt_bit1, ennreal.bit1_le_bit1, ennreal.bit1_top;
  • ennreal.div_eq_inv_mul, ennreal.of_real_mul';
  • filter.eventually.prod_nhds.

Generalize lemmas

  • Drop unneeded assumption in real.to_nnreal_bit0 and ennreal.of_real_bit0.

Rename lemmas

  • ennreal.mul_div_cancel → ennreal.div_mul_cancel, fixing a TODO;
  • prod_is_open.mem_nhds → prod_mem_nhds: there are no open sets in the statement.

Other changes

  • Golf some proofs.
  • Avoid non-final simps here and there.
  • Move mul_inv_cancel etc up to use them in other proofs.
  • Move some to_nnreal lemmas above to_real lemmas, use them in to_real lemmas.
  • Use to_dual in order_iso.inv_ennreal.

Estimated changes

modified theorem ennreal.bit0_eq_top_iff
modified theorem ennreal.bit0_eq_zero_iff
modified theorem ennreal.bit0_inj
added theorem ennreal.bit0_injective
added theorem ennreal.bit0_le_bit0
added theorem ennreal.bit0_lt_bit0
added theorem ennreal.bit0_top
modified theorem ennreal.bit1_eq_one_iff
modified theorem ennreal.bit1_eq_top_iff
modified theorem ennreal.bit1_inj
added theorem ennreal.bit1_injective
added theorem ennreal.bit1_le_bit1
added theorem ennreal.bit1_lt_bit1
modified theorem ennreal.bit1_ne_zero
added theorem ennreal.bit1_top
added theorem ennreal.div_eq_inv_mul
added theorem ennreal.div_mul_cancel
modified theorem ennreal.inv_le_iff_le_mul
modified theorem ennreal.inv_le_inv
modified theorem ennreal.inv_lt_inv
deleted theorem ennreal.mul_div_cancel
modified theorem ennreal.mul_div_le
modified theorem ennreal.of_real_bit0
added theorem ennreal.of_real_mul'
modified theorem ennreal.to_nnreal_mul
modified theorem ennreal.to_nnreal_mul_top
modified theorem ennreal.to_nnreal_pow
modified theorem ennreal.to_nnreal_prod
modified theorem ennreal.to_nnreal_top_mul
modified theorem ennreal.to_real_mul
modified theorem ennreal.to_real_mul_top
modified theorem ennreal.to_real_pow
modified theorem ennreal.to_real_prod
modified theorem ennreal.to_real_top_mul
modified theorem real.to_nnreal_bit0
deleted theorem prod_is_open.mem_nhds
added theorem prod_mem_nhds