While trying to the proofs about continuous inverses into normedtype.v
, I encountered the problem that my proof uses near_shift
, which is only defined in landau.v
, which depends on normedtype.v
. So it seems a specialized file for real analysis will be needed. It was mentioned that the trigonometry functions would also go in that file. What name should we choose?
real_fun.v was heard during the last meeting :-)
I'd prefer realfun.v
Last updated: Oct 13 2024 at 01:02 UTC