Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-16 11:29 21a387fe

View on Github →

feat(algebra/order/monoid_lemmas): add antitone, monotone_on, and antitone_on lemmas (#15267)

Estimated changes

Modified src/algebra/order/monoid_lemmas.lean

added theorem antitone.const_mul'

added theorem antitone.mul'

added theorem antitone.mul_const'

added theorem antitone.mul_strict_anti'

added theorem antitone_on.const_mul'

added theorem antitone_on.mul'

added theorem antitone_on.mul_const'

added theorem antitone_on.mul_strict_anti'

added theorem monotone_on.const_mul'

added theorem monotone_on.mul'

added theorem monotone_on.mul_const'

added theorem monotone_on.mul_strict_mono'

added theorem strict_anti.const_mul'

added theorem strict_anti.mul'

added theorem strict_anti.mul_antitone'

added theorem strict_anti.mul_const'

added theorem strict_anti_on.const_mul'

added theorem strict_anti_on.mul'

added theorem strict_anti_on.mul_antitone'

added theorem strict_anti_on.mul_const'

modified theorem strict_mono.const_mul'

modified theorem strict_mono.mul_const'

added theorem strict_mono_on.const_mul'

added theorem strict_mono_on.mul'

added theorem strict_mono_on.mul_const'

added theorem strict_mono_on.mul_monotone'