Stream: math-comp analysis

Topic: Creating a file for real analysis


view this post on Zulip Yves Bertot (Jul 23 2021 at 14:14):

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?

view this post on Zulip Reynald Affeldt (Jul 23 2021 at 14:27):

real_fun.v was heard during the last meeting :-)

view this post on Zulip Cyril Cohen (Jul 25 2021 at 20:17):

I'd prefer realfun.v


Last updated: Aug 19 2022 at 20:03 UTC