Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-09 05:36 df5eddeb

View on Github →

refactor(strict_mono): make definition + move to order_functions (#998)

  • refactor(strict_mono): make definition + move to order_functions
  • Weaken assumptions from preorder to has_lt

Estimated changes

deleted theorem injective_of_strict_mono
deleted theorem le_iff_le_of_strict_mono
deleted theorem lt_iff_lt_of_strict_mono
added theorem strict_mono.compares
added theorem strict_mono.injective
added theorem strict_mono.le_iff_le
added theorem strict_mono.lt_iff_lt
added theorem strict_mono.monotone
added def strict_mono