COUNTABLE_LIST_UNIV (new) and CARD_COUNTABLE_CONG (fixed)

[binghe]

Hi,

In cardinalTheory, the following two existing theorems saying two sets are both countable if they have the same cardinality, are fixed (trivially) by making the two involved sets type-different (the type of t was :'a -> bool, rendering the theorems less useful):

> CARD_EQ_COUNTABLE;
val it = |- !(s :'a -> bool) (t :'b -> bool). countable t /\ s =~ t ==> countable s: thm
> CARD_COUNTABLE_CONG;
val it = |- !(s :'a -> bool) (t :'b -> bool). s =~ t ==> (countable s <=> countable t): thm

I found this issue when I was trying to use them on two sets having different types. Then, I added the following two new theorems about the cardinality of the universe of all lists:

   [COUNTABLE_LIST_UNIV]  Theorem      
      ⊢ countable 𝕌(:α) ⇒ countable 𝕌(:α list)
   
   [COUNTABLE_LIST_UNIV']  Theorem      
      ⊢ FINITE 𝕌(:α) ⇒ countable 𝕌(:α list)

The proof of the above first theorem heavily relies on the list constant in cardinalTheory and several advanced set-theoretic results there.

The above second one is an easy corollary of the first one (because FINITE_IMP_COUNTABLE |- ∀s. FINITE s ⇒ countable s) but is actually more useful. For example, with FINITE_UNIV_char ⊢ FINITE 𝕌(:char), one can easily prove COUNTABLE_STR_UNIV ⊢ countable 𝕌(:string) (but there's no good place to put this theorem, as stringTheory is built much earlier than cardinalTheory.)

P. S. COUNTABLE_STR_UNIV is currently in basic_swapTheory of the lambda example.

--Chun

[binghe]

The changes of CARD_EQ_COUNTABLE has caused one broken proof in real_topologyTheory, where a call of SPEC must be changed to ISPEC. I don't know if there are other broken proofs during the CI tests but let's see.

[mn200]

Thanks!