search

math-comp / analysis

Mathematical Components compliant Analysis Library
Other
203 stars 45 forks source link

naming and definition of `monotonous` #1133

Open affeldt-aist opened 9 months ago

affeldt-aist commented 9 months ago

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 commented 7 months ago

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