Dear friends, how do you usually express the largest integer or natural number that subjects to some condition?
GREATEST x. P; so you write, for example,
GREATEST n :: nat. n < 1000.
It should work with all types that are instances of
ord. I used it for relations, which are only partially ordered.
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.
For what it's worth, I have (more or less copied) the lemmas in
arg_max (and primarily
arg_max_on) which are there for
Last updated: Dec 07 2023 at 12:30 UTC