Stream: math-comp users

Topic: \min


view this post on Zulip Pierre Jouvelot (Apr 07 2022 at 12:49):

Is there a particular reason why there is no \min in bigop.v or order.v (just a reserved notation)?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2022 at 12:49):

I guess it is hard to pick the neutral element?

view this post on Zulip Pierre Jouvelot (Apr 07 2022 at 12:50):

Not for nat.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2022 at 12:50):

For nat there is no neutral element, right?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2022 at 12:51):

what would it be?

view this post on Zulip Pierre Jouvelot (Apr 07 2022 at 12:52):

Indeed. There would be an absorbing one. Still, \min could be useful for non-empty sets/lists.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2022 at 13:11):

Yes I guess that's why the notation is reserved, so users can instantiate it if they have a bound

view this post on Zulip Pierre Jouvelot (Apr 07 2022 at 13:13):

I see. Thanks.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2022 at 13:13):

For order.v tho, it should be avaiable when the lattice has top

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2022 at 13:14):

If it is not, I guess that's a todo


Last updated: Jan 29 2023 at 18:03 UTC