Commit 2021-12-21 07:22 2ceda785

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.