Zulip Chat Archive

Stream: general

Topic: monotonicity lemma


view this post on Zulip 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: May 15 2021 at 23:13 UTC