On Jun 15, 2:57 am, Jan Burse <janbu...@fastmail.fm> wrote: > Dan Christensen schrieb: > > > Full text at:http://dcproof.com/CBS.htm From the informal > > introduction: > > > THEOREM (Cantor-Bernstein-Schroeder): > > gr8 work! Congratulations. >
> The proof has >1000 lines, could it be made shorter? >
Currently at 1,262 lines, it could be made a little shorter. I might be able to get it under 1000. I will be going through the proof at a later date to see if I can make some improvements.
> When I was googling I found different operators used > to yield a fixpoint. The one you were using is found > on the french wikipedia side, another one is shown > on the german wikipedia side. >
I have a proof of the fixed-point theorem as well (241 lines). I hope to be releasing it, along with a collection of proofs on orders of infinity, with an update of my program this summer.