prove cnplimc in iset.mm #3638
prove cnplimc in iset.mm #3638
Conversation
Specifically, use xmetres2 in place of xmetres . This takes the size in SHOW PROOF/SIZE from 3263 characters to 3125.
This is cnplimc from set.mm with different notation for the topology on the complex numbers. The forward direction is cnplimcim which we had already. The reverse direction is a new proof by Mario Carneiro, formalized by Jim Kingdon, which is in new lemmas cnplimclemle and cnplimclemr .
Stated as in set.mm. The proof is similar to the set.mm proof with adjustments for the notation of the topology on the complex numbers.
This is for recent changes in iset.mm related to cnlimc , limccnp2 and cnplimc
jkingdon
force-pushed
the
limccnp2cntop-shorten
branch
from
a4a73d9 to
4b2fb0a
Compare
A little note: SHOW PROOF /SIZE is bugged metamath/metamath-exe#137 (comment). If you want to know the true size of a compressed proof I recommend using SHOW PROOF /COMPRESSED instead (at the end of the proof metamath-exe always shows the proof length). So in your case the size of |
Ah yeah, thanks for the analysis. Most of the proof shortenings I do will end up shorter using any of our various ways of measuring it, but if I do post numbers next time I'll try to remember about SHOW PROOF /COMPRESSED. |
Fixes #3634 (see discussion there)