Stream: Is there code for X?

Topic: Largest integer that subjets to ...


view this post on Zulip Qiyuan Xu (Jan 19 2023 at 08:13):

Dear friends, how do you usually express the largest integer or natural number that subjects to some condition?

view this post on Zulip Wolfgang Jeltsch (Jan 19 2023 at 12:28):

With GREATEST x. P; so you write, for example, GREATEST n :: nat. n < 1000.

view this post on Zulip Wolfgang Jeltsch (Jan 19 2023 at 12:30):

It should work with all types that are instances of ord. I used it for relations, which are only partially ordered.

view this post on Zulip Manuel Eberl (Jan 19 2023 at 22:17):

There's also Sup and Max and arg_max. I would typically use Max I think, but GREATEST also works of course.

arg_max unfortunately has a lot of missing lemmas so it is of limited use.

view this post on Zulip Christoph Madlener (Jan 20 2023 at 11:20):

For what it's worth, I have (more or less copied) the lemmas in Lattices-Big.thy for arg_max (and primarily arg_max_on) which are there for arg_min (resp. arg_min_on) here.


Last updated: Mar 28 2024 at 12:29 UTC