Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-03 20:14 545dd03d

View on Github →

feat(topology/metric_space/antilipschitz): define antilipschitz_with (#2075)

  • chore(data/real/ennreal): weaker assumptions in sub_mul, add coe_inv_le
  • feat(topology/metric_space/antilipschitz): define antilipschitz_with Also make some proofs use facts about antilipschitz_with.
  • Rename inequalities, move K to the other side This way it's easier to glue it with the rest of the library, and we can avoid assuming 0 < K in many lemmas.

Estimated changes

added theorem edist_add_add_le
added theorem lipschitz_with.add
added theorem lipschitz_with.neg
added theorem lipschitz_with.sub
added theorem nndist_add_add_le
added theorem antilipschitz_with.id
deleted theorem contracting_with.dist_le
added theorem isometry.antilipschitz
modified theorem isometry.injective
added theorem isometry.lipschitz
deleted theorem lipschitz_with.edist_le