Re: [ProofPower] bijection between N adn N x N

2011-01-15 Thread Roger Bishop Jones
On Saturday 15 Jan 2011 13:47, Rob Arthan wrote: > On 11 Jan 2011, at 12:03, Roger Bishop Jones wrote: > > Do you intend to add this to maths_egs? > > It was originally destined for inclusion in ProofPower > itself as part of a recursive type definition package, > but I keep failing to getting r

Re: [ProofPower] bijection between N adn N x N

2011-01-15 Thread Rob Arthan
Roger, On 11 Jan 2011, at 12:03, Roger Bishop Jones wrote: > Thanks Rob, that's great. > > Do you intend to add this to maths_egs? It was originally destined for inclusion in ProofPower itself as part of a recursive type definition package, but I keep failing to getting round to that. Regards

Re: [ProofPower] bijection between N adn N x N

2011-01-11 Thread Roger Bishop Jones
Thanks Rob, that's great. Do you intend to add this to maths_egs? Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] bijection between N adn N x N

2011-01-11 Thread Rob Arthan
As I thought, the mailing list scrubbed the attachment (at least in the archive). If anyone else wants this, let me know and I will e-mail you direct. Regards, Rob. On 11 Jan 2011, at 10:47, Rob Arthan wrote: > Roger, > > See attached. > > Regards, > > Rob. > > On 11 Jan 2011, at 09:14, Ro

Re: [ProofPower] bijection between N adn N x N

2011-01-11 Thread Rob Arthan
Roger, See attached. Regards, Rob. rec.tgz Description: Binary data On 11 Jan 2011, at 09:14, Roger Bishop Jones wrote: > Does anyone have a proof in ProofPower of a bijection > between N and N x N. > Or even an injection from N x N to N? > > Roger Jones > > __