Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-14 03:22 c928e34d

View on Github →

feat(data/real/ennreal,topology/*): assorted lemmas (#6663)

  • add @[simp] to ennreal.coe_nat_lt_coe_nat and ennreal.coe_nat_le_coe_nat;
  • add ennreal.le_of_add_le_add_right;
  • add set.nonempty.preimage;
  • add ennreal.infi_mul_left' and ennreal.infi_mul_right';
  • add ennreal.tsum_top;
  • add emetric.diam_closure;
  • add edist_pos;
  • add isometric.bijective, isometric.injective, and isometric.surjective.

Estimated changes

modified theorem ennreal.coe_nat_le_coe_nat
modified theorem ennreal.coe_nat_lt_coe_nat
added theorem set.nonempty.preimage
added theorem emetric.diam_closure
added theorem ennreal.infi_mul_left'
added theorem edist_pos