map_nonneg

Stream: mathlib4

[Yury G. Kudryashov]

We have docs#map_nonneg (about docs#OrderAddMonoidHomClass) and docs#NonnegHomClass.map_nonneg (exported to the root namespace). #10472 changes imports so that both are available in many files. Which one should stay in the root namespace?

[Yaël Dillies]

One of them could be map_nonneg while the other one could be apply_nonneg?

[Yury G. Kudryashov]

One can be map_nonneg, another can be map_nonneg_of_nonneg...

[Yaël Dillies]

What I mean is that one of them "maps" the nonnegativity assumption, the other one creates it.

[Yury G. Kudryashov]

So, should I rename NonnegHomClass.map_nonneg to apply_nonneg and mention it in the map_nonneg docstring?

[Yaël Dillies]

Sounds good

[Yury G. Kudryashov]

#10507