Email Gateway (Aug 18 2022 at 16:41): Email Gateway (Aug 18 2022 at 16:41):From: Victor Porton <porton@narod.ru>
I am writing my first theory.
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?
\--
Victor Porton - http://portonvictor.org
Email Gateway (Aug 18 2022 at 16:41):From: Alexander Krauss <krauss@in.tum.de>
Hi Victor,
we'll certainly take contributions.
Alex
Last updated: Nov 21 2024 at 12:39 UTC