Zulip Chat Archive
Stream: Is there code for X?
Topic: strict mono f on well-order → x ≤ f x
Violeta Hernández (Dec 12 2021 at 00:46):
As the title suggests
Violeta Hernández (Dec 12 2021 at 00:47):
The proof is simple enough: suppose otherwise, take the least x such that f x < x, so therefore f (f x) < f x < x, contradiction.
Yury G. Kudryashov (Dec 12 2021 at 00:57):
We have this for nat but I don't think that we have it for any well-order.
Violeta Hernández (Dec 12 2021 at 01:01):
@Yury G. Kudryashov What's the name of that result?
Yury G. Kudryashov (Dec 12 2021 at 01:10):
Violeta Hernández (Dec 12 2021 at 03:24):
Just made a PR: #10732
Last updated: Dec 20 2023 at 11:08 UTC