analysis icon indicating copy to clipboard operation
analysis copied to clipboard

Published 20 hours ago • verified publisher icon math-comp

naming and definition of `monotonous`

Open affeldt-aist opened this issue 1 year ago • 1 comments

https://github.com/math-comp/analysis/blob/437d12c836f530fe5dfc8a26e7330b2653d175a3/classical/mathcomp_extra.v#L1491

"According to WP (https://en.wikipedia.org/wiki/Monotonic_function), this should rather be monotonic and I would expect it to be non strict (with homo instead of mono). Maybe we should also have a strict version. I would also expect it to use nondecreasing_fun and the like from realfun.v. All in all, maybe this change should come in a separate PR so as to not delay the remaining of the current PR." @proux01

affeldt-aist avatar Jan 07 '24 15:01 affeldt-aist

NB: fixing this issue depends on this PR to MathComp https://github.com/math-comp/math-comp/pull/1179

affeldt-aist avatar Mar 14 '24 15:03 affeldt-aist