Stream: math-comp users

Topic: MC2.1 substitution for bigmaxr

view this post on Zulip Yichen Tao (Apr 03 2024 at 16:41):

I am trying to port a repo to mathcomp 2.1, while I found that the definition bigmaxr is deprecated. It is suggested by mathcomp 2.1 to "Use topology.v's bigmax/min lemmas instead". However, there aren't many relevant lemmas in the bigmax/min section in file topology.v. Actually I only found four lemmas that "reflects" the boolean and prop definitions.
Can anyone point me to the lemmas that corresponds to those lemma like bigmaxrP that were present in previous versions of mathcomp? Any suggestion or insight will be greatly appreciated!

view this post on Zulip Reynald Affeldt (Apr 03 2024 at 21:54):

I am not sure (and cannot check right now) but maybe this is due to an old comment that redirects you to topology.v. The lemmas about bigmax/bigmin that used to live there have been generalized and moved to ssreflect/order.v in the meantime.

view this post on Zulip Yichen Tao (Apr 04 2024 at 19:00):

Thank you so much! I found the lemmas that I'm using. Your suggestion is really helpful!

Last updated: Jul 15 2024 at 20:02 UTC