Email Gateway (Aug 18 2022 at 16:08): Email Gateway (Aug 18 2022 at 16:08):From: Joachim Breitner <mail@joachim-breitner.de>
Hi again,
I discovered that the ZF logic has some good coverage of cardinality,
(including schroeder_bernstein) and the following theorem which seems to
implies the statement above (using K=nat and X(i) the words of length i)
lemma cardinal_UN_le:
"[| InfCard(K); ALL i:K. |X(i)| le K |] ==> |\<Union>i∈K. X(i)| le K"
But looking at the amount of work done to get there, it looks as if it
is too hard to re-do it in HOL. Am I right to assume that there is no
sensible way of using results from ZF in HOL?
Maybe I can try the result above at least for countable infinite M in
HOL.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 18 2022 at 16:09):From: Joachim Breitner <mail@joachim-breitner.de>
Hi Brian,
thanks for the pointer. I wasn’t aware of HOL/Library, and I’ll make
sure to look there the next time as well. HOL/Library/Countable looks
interesting as well.
I’d like to know of a way to proof this for uncountable sets as well
before digging into this, though. Having the result only for nat is not
very exciting.
Greetings,
Joachim
signature.asc
Last updated: Apr 19 2024 at 04:17 UTC