Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-29 13:45 8f11c466

View on Github →

feat(data/real/ennreal): more simp lemmas about inv and continuity of inv (#1749)

  • Prove some algebraic properties of ennreal.inv
  • More algebraic lemmas
  • Prove continuity of inv

Estimated changes

modified theorem ennreal.coe_one
modified theorem ennreal.coe_zero
added theorem ennreal.inv_bijective
added theorem ennreal.inv_eq_inv
added theorem ennreal.inv_involutive
added theorem ennreal.inv_le_inv
added theorem ennreal.inv_lt_inv
added theorem ennreal.inv_pos