mathlib3

2ceda785 - feat(order/monovary): Monovariance of a pair of functions. (#10890)

feat(order/monovary): Monovariance of a pair of functions. (#10890) `f` monovaries with `g` if `g i < g j → f i ≤ f j`. `f` antivaries with `g` if `g i < g j → f j ≤ f i`. This is a way to talk about functions being monotone together, without needing an order on the index type.