Zulip Chat Archive

Stream: general

Topic: monotonicity lemma


Rob Lewis (Sep 28 2018 at 13:00):

I feel like this lemma (or similar) must exist somewhere already, but I'm coming up empty -- anyone recognize this?

example {α} [partial_order α] (f :   α) (h :  n, f (n+1)  f n) :  m n, m  n  f n  f m

Last updated: Dec 20 2023 at 11:08 UTC