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 :-)
Last updated: Feb 05 2023 at 07:03 UTC