mathlib
bf25d26f - chore(data/set/intervals/proj_Icc): add `strict_mono_incr_on` (#5292)

Commit
5 years ago
chore(data/set/intervals/proj_Icc): add `strict_mono_incr_on` (#5292) * rename `set.Icc_extend_monotone` to `monotone.Icc_extend`; * add `set.strict_mono_incr_on_proj_Icc` and `strict_mono.strict_mono_incr_on_Icc_extend`.
Author
Parents
Loading