mathlib
f855a4ba - feat(order/monotone): Monotonicity of `prod.map` (#14843)

Commit

3 years ago

feat(order/monotone): Monotonicity of `prod.map` (#14843) If `f` and `g` are monotone/antitone, then `prod.map f g` is as well.

Author

YaelDillies

Parents