Set construction proof basics

Stream: new members

[Alexa McLain]

Hello, I am trying to build up bit by bit a formalization of a natural language proof as a means of learning Lean. Here's the problem statement: "Let A ⊂ R^n be an infinite closed subset. Show there exists a countable dense subset of A." The first step of the proof involves invoking the fact that R^n contains a dense countable subset, Q, where Q ⊂ R^n is the set of all points with rational coordinates. For debugging I am trying to prove a limited claim about Q [that Q is a countable dense subset of A], can someone tell me where I am going wrong in completing the proof?

import Mathlib.Topology.MetricSpace.Basic
import Mathlib.Topology.Instances.Real
import Mathlib.Data.Set.Countable
import Mathlib.Data.Real.Basic
import Mathlib.Topology.Defs.Basic
import Mathlib.Topology.Instances.Rat

open Set

--Let A ⊂ R^n be an infinite closed subset
def is_infinite_closed_subset_of_real_space (A : Set (Fin n -> ℝ)) : Prop :=
  Infinite A ∧ IsClosed A

--Show there exists a countable dense subset of A
theorem exists_countable_dense_subset
  {A : Set (Fin n -> ℝ)} (hA : is_infinite_closed_subset_of_real_space A) :
  ∃ Q : Set (Fin n -> ℝ), Countable Q ∧ Q ⊆ A :=

  --Define Q ⊂ R^n as the dense, countable subset of all points with rational coordinates
  let Q : Set (Fin n-> ℝ) := A ∩ {q | ∀ i, ∃ r : ℚ, q i = r}

  have rationals_dense_in_reals : Dense {(x : ℝ) | (x : ℚ)} :=
  Rat.denseEmbedding_coe_real.dense

  have rationals_countable : (Set.univ : Set ℚ).Countable :=
  Set.countable_rat

  have rationals_dense_countable :
  Dense {x : ℝ | ∃ q : ℚ, x = q} ∧ (Set.univ : Set ℚ).Countable := by
    constructor
    exact rationals_dense_in_reals
    exact rationals_countable

{Q, rationals_dense_in_reals}

[Luigi Massacci]

Are you sure your limited claim is true?

[Luigi Massacci]

I don't think closed subsets of $\mathbb{R}$ need to contain any rational points at all, you can probably fiddle with the Cantor set construction to get a counterexample

[Luigi Massacci]

Of course the broader theorem remains true, you can get it by composing docs#TopologicalSpace.Subtype.secondCountableTopology (which is arguably the "main" part of the claim) and docs#TopologicalSpace.SecondCountableTopology.to_separableSpace

[Luigi Massacci]

plus the fact that the usual topology on the reals is second countable docs#instSecondCountableTopologyReal

[Alexa McLain]

Thanks for your feedback. Can you clarify what you mean by limited claim is true? Do you mean the problem statement is formalized incorrectly?

[Luigi Massacci]

Your limited statement (as you seem to have phrased it in words, and as it seems your formalisation is trying to prove) is that for any infinite closed subset of $\mathbb{R}$, it contains a countable dense subset that is made by its rational subpoints. This is not true in my opinion, you can have closed infinite subsets that contain no rational points. I hope this is clearer

[Luigi Massacci]

In other words: there are $A \subset \mathbb{R}$ for which Q, as you defined it in the lean code, is empty

[Alexa McLain]

Ah I see. Hmm, trying to reconcile this with your second point about the broader theorem being true. So really the definition of Q just needs to be refined to be non-empty? As in exclude the places where the intersection with A is empty

[Luigi Massacci]

No, it's just that you can't hope to construct your countable subset that way, it's a bit more involved than that

[Alexa McLain]

Sorry, I'm not sure I'm following. What should I change to be able to draw on the known properties of rationals being dense in reals from mathlib?

[Luigi Massacci]

Can I ask what your paper proof of the main statement is like?

[Alexa McLain]

Sure, see attached
image.png

[Luigi Massacci]

See, in the construction when they take the intersection with $A$ to define $S(q, k)$, notice how they are taking the intersection with the ball centered on $q$, and when they pick out $y_{q, k}$, they make no assumption that it is rational. Likewise in the proof of density, they pick some element $s$, and only argue that by construction it must be close to some rational, but not necessarily itself rational

[Alexa McLain]

Aren’t the balls centered at points drawn from Q which means they have rational coordinates?

[Alexa McLain]

In terms of y and s I agree with your interpretation

[Luigi Massacci]

only the center is rational

[Alexa McLain]

Correct. I guess my question is how to reflect that best in Lean

[Luigi Massacci]

Do you need help defining $S(q, k)$ then?

[Alexa McLain]

Oh actually I see the issue here now that you’re pointing out is coming from how I truncated it

[Alexa McLain]

I guess there are two things. In what I shared above I am not trying to reconstruct the whole proof, just use Q as an existence to get something end to end working

[Alexa McLain]

If you give me 15 minutes I’ll be back in front of my computer and can share code that defines S

[Luigi Massacci]

of course the one above is not a counterexample to the limited claim you made (which is rather more complicated to construct), but the reason the proof goes through all this trouble is because it is necessary. Otherwise they could just use $\mathbb{Q}$ itself and save a lot of time

[Alexa McLain]

Here you go: (low confidence this is correct, hence previous attempt to introduce modularity)

 --Define Q ⊂ R^n as the dense, countable subset of all points with rational coordinates
  let Q : Set (Fin n-> ℝ) := A ∩ {q | ∀ i, ∃ r : ℚ, q i = r}

  have hBall (x : Fin n → ℝ) (ε : ℝ) : Metric.ball x ε = {y | dist y x < ε} := by rfl

  let N_pos : Set ℕ := {n : ℕ | n > 0}
  let QxN_pos : Set (Q × N_pos) := Set.prod Q {n : ℕ | n > 0}
  let S : (Set (Fin n -> ℝ) × ℕ) → Set (Fin n -> ℝ) := λ (q, k) => A ∩ Metric.ball q (1 / k)

  let B : Set ((Fin n -> ℝ) × ℕ) :={ (q, k) | (q, k) ∈ QxN_pos ∧ ¬(S (q, k)).isEmpty }