Countable Union of Countable Sets is Countable

Stream: new members

[Ethan Barry]

Hello! I'm struggling with formalizing the statement of this theorem. I haven't really played with sets and countability in Lean, as I'm just getting into it, so please pardon my ignorance.

I'd like to state this theorem:

A countable union of countable sets is countable.

I see that this theorem already exists in Mathlib at Set.countable_iUnion, and I believe I understand what it's doing.

However, I'd like to prove this via induction, and ι is not an inductive type in that context. If I could just index with natural numbers instead, that would be nice. (I know induction is unnecessary, but I'm a CS major and I'm determined to use it wherever possible!)

My intended English proof and current Lean MWE follow:

Proof: By induction on n. If n is 0, then

$$\bigcup_{i\in \{0\}} A_i = A_0$$

which is countable by hypothesis.
Assuming the proposition is true up to some n, we show it is true for n + 1. We know the union of A_i over 0 to n is a countable set, and we know that the union of any two countable sets is countable. (I've already proved that in my project.) Thus

$$\left[\bigcup_{i\in\{0,...,n\}} A_i\right] \cup A_{n+1}$$

is a countable set.

import Mathlib.Data.Nat.Basic
import Mathlib.Data.Set.Basic
import Mathlib.Tactic

universe u v
variable {α : Type u}

theorem countable_union_of_countables {t : ℕ → Set α} {i : ℕ}
  (ht : ∀ i, (t i).Countable)
: (⋃ i, t i).Countable := by
  induction i with
  | zero => simp; exact ht
  | succ i ih => exact ih

I can't help but feeling I have proved the wrong thing, which is why I think my statement is wrong. I never had to invoke the other theorem about the union of two countable sets. Have I just assumed the conclusion somehow? Is my induction flawed? Or did I break everything when I made i an implicit variable with {i : ℕ}?

EDIT: I'm certain something is wrong, because simp; exact ht suffices in the inductive case, which never invokes the inductive hypothesis. I believe that means the induction is garbage.

[Weiyi Wang]

The {i : ℕ} parameter in the statement is what makes it wrong, I think Let me think again...

[Mirek Olšák]

I have a feeling that the mathematical proof is wrong. This way, you could prove by induction that a countable union of finite sets is finite, because union of two finite sets is finite.

[Weiyi Wang]

Ok so there are multiple thing that goes wrong:

• The {i : ℕ} parameter shouldn't appear in the statement
• simp is the load-bearing part that does all the hard work for you. It invokes Set.countable_iUnion_iff which is what you wanted to avoid

[Ethan Barry]

Weiyi Wang said:

Ok so there are multiple thing that goes wrong:

• The {i : ℕ} parameter shouldn't appear in the statement
• simp is the load-bearing part that does all the hard work for you. It invokes Set.countable_iUnion_iff which is what you wanted to avoid

Ah, that makes sense; of course simp is invoking that. Why wouldn't it? Now in the library, it declares ι is countable with [Countable ι]. What is that syntax? Is that leaving ι as a general "range" or something? I guess {i : ℕ} chooses a particular i, right?

[Weiyi Wang]

[Countable ι] is a type class parameter. It is similar to (_ : Countable ι), but it is filled in implicitly by the type class search engine. Mathlib proved Countable ℕ somewhere so it automatically inserted it for you

[Weiyi Wang]

As for simp, you can do simp? to see what theorems it used

[Aaron Liu]

you seem to have proven by induction that the finite union of countable sets is countable

[Ethan Barry]

Aaron Liu said:

you seem to have proven by induction that the finite union of countable sets is countable

Ah, that resolves what @Mirek Olšák said. I guess I'm not proving it for a countably infinite number of sets. I see!

[Ethan Barry]

Is there any logical leap that takes me from proving it for an arbitrary finite number of sets to a countably infinite number?

[Weiyi Wang]

Transfinite induction / Zorn's lemma is similar to that leap but probably not necessary here

[Mirek Olšák]

I am afraid that the leap is quite significant. You have proven that A1 is countable, A1 + A2 is countable, A1 + A2 + A3 is countable, ... so you could hope that when this infinite nested sequence of sets is countable, the full union is "trivially" countable too. Unfortunatelly, instead of being trivial, it translates back to the original problem -- you are taking an union of infinitely many countable sets, and you want the union to be countable.

[Mirek Olšák]

I don't know a proof of "countable union of nested countable sets is countable" which would be any easier than the original problem.

[Ethan Barry]

Weiyi Wang said:

Transfinite induction / Zorn's lemma is similar to that leap but probably not necessary here

So basically WOP/AC? That's getting outside the scope of my Foundations course, I believe. :laughing:

Mirek Olšák said:

it translates back to the original problem

Ah, OK. I'm going in circles, then. That makes sense, I guess. We proved this theorem by diagonalization in class, and I may be over-optimistic in thinking something less powerful than diagonalization can prove this statement.

[Mirek Olšák]

Weiyi Wang said:

Transfinite induction / Zorn's lemma is similar to that leap but probably not necessary here

That sounds like some magical words to scare children :smiley: , there is no need for it, nor any use for it in this case.

[Ethan Barry]

Mirek Olšák said:

That sounds like some magical words to scare children

That's still most of higher mathematics for me at this point, I'm afraid! :rolling_on_the_floor_laughing:

[Mirek Olšák]

Ah, OK. I'm going in circles, then. That makes sense, I guess. We proved this theorem by diagonalization in class, and I may be over-optimistic in thinking something less powerful than diagonalization can prove this statement.

Yes, I think the easiest way to prove it is to provide an explicit injection ℕ × ℕ → ℕ.

[Ethan Barry]

Well, if diagonalization is what I need, then I guess I'd better see how to do this in Lean. Do you all know of any examples where something like this is stated in Mathlib?

[Mirek Olšák]

Ethan Barry said:

Weiyi Wang said:

Transfinite induction / Zorn's lemma is similar to that leap but probably not necessary here

So basically WOP/AC? That's getting outside the scope of my Foundations course, I believe. :laughing:

Happy to recommend my video series on Set Theory ;-)

[Ethan Barry]

Mirek Olšák said:

Happy to recommend my video series on Set Theory ;-)

Holy smokes! And all in Manim, too! I'll be watching these; thank you so much.

[Mirek Olšák]

Ethan Barry said:

Well, if diagonalization is what I need, then I guess I'd better see how to do this in Lean. Do you all know of any examples where something like this is stated in Mathlib?

Mathlib does this through the functions Nat.pair & Nat.unpair, which are combined into Nat.pairEquiv

[Mirek Olšák]

In my second video, I actually did it "almost" by induction on pairs, but one needs to be more careful to state that rigorously. It is not about proving inductively some statement but recursively building the function ℕ × ℕ → ℕ.