Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nnreal.inv_lt_inv

Modification history

2022-01-22 22:28
src/data/real/nnreal.lean
feat(topology/instances/ennreal): continuity of subtraction on ennreal (#11527)
Added nnreal.inv_lt_invView on Github →