Mathlib v3 is deprecated. Go to Mathlib v4

Theorem strict_mono.cod_restrict

Modification history

2020-12-09 04:36
src/data/set/function.lean
feat(analysis/special_functions): `real.log` is infinitely smooth away from zero (#5116) …
Added strict_mono.cod_restrictView on Github →