Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-27 10:29 850784cf

View on Github →

chore(order/*): rename strict_mono_{incr,decr}_on to strict_{mono,anti}_on (#9401) This was done as a direct find and replace

Estimated changes

deleted theorem strict_mono_incr_on_pow
added theorem strict_mono_on_pow
added theorem one_div_strict_anti_on
modified theorem real.inj_on_cos
modified theorem real.arccos_inj_on
modified theorem real.inj_on_arcsin
added theorem strict_anti_on.inj_on
deleted theorem strict_mono_incr_on.comp
added theorem strict_mono_on.comp
added theorem strict_mono_on.inj_on
added def strict_anti_on
deleted def strict_mono_decr_on
deleted def strict_mono_incr_on
added def strict_mono_on