Stream: Beginner Questions

Topic: infinite type 'a has an injection (nat * 'a) -> 'a

Yiming Xu (Feb 05 2025 at 13:32):

Do we have any existing theorem saying that we can embed the product (nat * 'a) back to 'a given that 'a is infinite?

If there is not, may I please ask for the easiest way to prove it?

Maybe something like:
-for infinite 'a we have 'a \times 'a injects to 'a
-for infinite 'a we have nat injects to 'a
-so we have nat \times 'a -> 'a \times \a -> 'a

But do the lemmas exist somewhere...?

Balazs Toth (Feb 05 2025 at 16:09):

A student of mine worked with this kind of lemmas. He used "HOL-Cardinals.Cardinals"

Christian Pardillo Laursen (Feb 05 2025 at 21:54):

Here's a generalised version of your theorem, using HOL-Library.Countable_Set:

lemma
  fixes X :: "'a set"
  assumes "infinite X" "countable Y" "Y ≠ {}"
  shows "∃f. bij_betw f (Y × X) X"
  apply (subst card_of_ordIso)
  apply (rule card_of_Times_infinite[OF assms(1,3), THEN conjunct2])
  by (meson assms card_of_ordLeqI countableE infinite_iff_card_of_nat iso_tuple_UNIV_I ordLeq_transitive)

Christian Pardillo Laursen (Feb 05 2025 at 21:54):

Turns out that the lemmas you wanted were in HOL/BNF_Wellorder_Constructions.thy

Yiming Xu (Feb 06 2025 at 11:52):

Christian Pardillo Laursen said:

Turns out that the lemmas you wanted were in HOL/BNF_Wellorder_Constructions.thy

Thanks so much for answering! I imported HOL-Library.Countable_Set and your proof already works. What should I know about HOL/BNF_Wellorder_Constructions.thy? The theorems there are mostly about ordering.

Balazs Toth (Feb 06 2025 at 13:21):

BNF_Wellorder_Constructions.thy should have the versions of these lemmas that do not require countable

Yiming Xu (Feb 06 2025 at 13:23):

So instead of "countable", the above theorem

lemma
  fixes X :: "'a set"
  assumes "infinite X" "countable Y" "Y ≠ {}"
  shows "∃f. bij_betw f (Y × X) X"
  apply (subst card_of_ordIso)
  apply (rule card_of_Times_infinite[OF assms(1,3), THEN conjunct2])
  by (meson assms card_of_ordLeqI countableE infinite_iff_card_of_nat iso_tuple_UNIV_I ordLeq_transitive)

can be strengthened into infinite Y. Is that what BNF_Wellorder_Constructions.thy will give us?

Balazs Toth (Feb 06 2025 at 13:24):

Yes basically, but you will have the assumption "|Y| <= |X|"

Yiming Xu (Feb 06 2025 at 13:25):

That's helpful to know. Vielen Dank!

Last updated: Mar 09 2025 at 12:28 UTC