Zulip Chat Archive

Stream: Is there code for X?

Topic: Well-ordering of the integers


view this post on Zulip Heather Macbeth (Sep 29 2020 at 17:23):

Does mathlib have the max of a nonempty bounded-above subset of Z\mathbb{Z}?

example (s : set ) (h₁ : nonempty s) (h₂ : bdd_above s) :  k, is_greatest s k

view this post on Zulip Yury G. Kudryashov (Sep 29 2020 at 17:57):

docs#int.exists_greatest_of_bdd

view this post on Zulip Yury G. Kudryashov (Sep 29 2020 at 18:00):

Found by git grep bdd src/data/int

view this post on Zulip Heather Macbeth (Sep 29 2020 at 18:01):

Great, thank you!


Last updated: May 16 2021 at 05:21 UTC