Re: [isabelle] Modifying Isabelle/ZF core?



Hi Victor,

Sadly I have not found in Perm.thy a theorem which would prove (given sets "small" and "big") "embed: inj(small, range(embed))" and/or "embed: bij(small, range(embed))"
from
"embded: inj(small, big)"
What us to do with this theorem? Should I prove it as a lemma in my own theory? Should we modify Isabelle/ZF core to add that new theorem?

we'll certainly take contributions.

Alex





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.