Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-22 22:28 31db25b4

View on Github →

feat(topology/instances/ennreal): continuity of subtraction on ennreal (#11527)

Estimated changes

Modified src/data/real/ennreal.lean

added theorem ennreal.mul_inv

Modified src/data/real/nnreal.lean

added theorem nnreal.inv_lt_inv

added theorem nnreal.inv_lt_inv_iff

Modified src/topology/instances/ennreal.lean

added theorem ennreal.tendsto_sub