analysis icon indicating copy to clipboard operation
analysis copied to clipboard

Published 20 hours ago • verified publisher icon math-comp

remove Rstruct lemmas about bigmax?

Open affeldt-aist opened this issue 2 years ago • 0 comments

https://github.com/math-comp/analysis/blob/2ae3b628d12cacdc000c4cd70e6f3cae26ecf429/theories/Rstruct.v#L502-L671

It looks like we do not use these lemmas anymore and since there are already bigmax/bigmin lemmas (see e.g. PR #712 ) in master should we think about removing this section?

affeldt-aist avatar Jul 29 '22 00:07 affeldt-aist