5.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

22 declarations, 14 contain sorry, 0 declared as axioms

Erdős Problem 5

References:

erdosproblems.com/5
[BFM16] Banks, William D. and Freiberg, Tristan and Maynard, James, On limit points of the sequence of normalized prime gaps. Proc. Lond. Math. Soc. (3) (2016), 515-539.
[Er55] Erdős, Paul, Some remarks on number theory. Riveon Lematematika (1955), 45-48.
[Er65b] Erdős, Paul, Some recent advances and current problems in number theory. Lectures on Modern Mathematics, Vol. III (1965), 196-244.
[Er85c] Erdős, P., On some of my problems in number theory I would most like to see solved. Number theory (Ootacamund, 1984) (1985), 74-84.
[Er97c] Erdős, Paul, Some of my favorite problems and results. The mathematics of Paul Erdős, I (1997), 47-67.
[GPY09] Goldston, Daniel A. and Pintz, János and Yıldırım, Cem Y., Primes in tuples. I. Ann. of Math. (2) (2009), 819-862.
[HiMa88] Hildebrand, Adolf and Maier, Helmut, Gaps between prime numbers. Proc. Amer. Math. Soc. (1988), 1-9.
[Me20] Merikoski, Jori, Limit points of normalized prime gaps. J. Lond. Math. Soc. (2) (2020), 99-124.
[Pi16] Pintz, János, Polignac numbers, conjectures of Erdős on gaps between primes, arithmetic progressions in primes, and the bounded gap conjecture. From arithmetic to zeta-functions (2016), 367-384.
[Ri56] Ricci, Giovanni, Recherches sur l'allure de la suite $\{p_{n+1}-p_n/\log p_n\}$. Colloque sur la Théorie des Nombres, Bruxelles, 1955 (1956), 93-106.
[We31] Westzynthius, E., Über die Verteilung der Zahlen, die zu den n ersten Primzahlen teilerfremd sind. Commentat. Phys. Math. (1931), 1-37.

Imports (1)

FormalConjecturesUtil

def Erdos5.normalizedGap The normalised prime gap $\frac{p_{n+1}-p_n}{\log n}$, where $p_n$ denotes the $n$-th prime line 59 source
Source documentation
The normalised prime gap $\frac{p_{n+1}-p_n}{\log n}$, where $p_n$ denotes the $n$-th prime.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: HDiv.hDiv, primeGap, Real.log
5 instances, coercions and auxiliary constants left out.
```
noncomputable def normalizedGap (n : ℕ) : ℝ := primeGap n / log n
```
Mentions: primeGap
def Erdos5.limitPointSet The set $S$ of limit points of $\frac{p_{n+1}-p_n}{\log n}$ line 72 source
Source documentation
The set $S$ of limit points of $\frac{p_{n+1}-p_n}{\log n}$.
Only the finite limit points are collected here; that $\infty$ is also a limit point is Westzynthius' theorem, recorded separately as erdos_5.variants.westzynthius.
Erdős' question, as well as [HiMa88] and [Pi16], normalises the prime gaps by $\log n$, whereas [GPY09], [BFM16] and [Me20] normalise by $\log p_n$. Since $\log p_n/\log n \to 1$ the two normalisations have the same limit points, so all the results below are stated for the normalisation used here.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Real
Proof uses: Set.ofPred, MapClusterPt, Nat, Filter.atTop, Erdos5.normalizedGap
4 instances, coercions and auxiliary constants left out.
```
def limitPointSet : Set ℝ := {x : ℝ | MapClusterPt x atTop normalizedGap}
…
```
Mentions: Erdos5.normalizedGap
theorem Erdos5.erdos_5 Let $C\geq 0$ sorry line 84 source
Source documentation
Let $C\geq 0$. Is there an infinite sequence of $n_i$ such that $$\lim_{i\to \infty}\frac{p_{n_i+1}-p_{n_i}}{\log n_i}=C?$$
We formalise "an infinite sequence of $n_i$" as a strictly monotone sequence of indices n : ℕ → ℕ. Note that the numerator is the gap between the two consecutive primes $p_{n_i}$ and $p_{n_i+1}$, which is primeGap (n i), and not the gap between the primes indexed by two consecutive members of the sequence.

depends on sorry what this means
Statement uses: Iff, True, Real, LE.le, OfNat.ofNat, Exists, Nat, And, StrictMono, Filter.Tendsto, Erdos5.normalizedGap, Filter.atTop, nhds
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_5 : answer(sorry) ↔ ∀ C : ℝ, 0 ≤ C →
    ∃ n : ℕ → ℕ, StrictMono n ∧ Tendsto (fun i => normalizedGap (n i)) atTop (𝓝 C) := by
…
```
Mentions: Erdos5.normalizedGap
theorem Erdos5.erdos_5.variants.limit_point_set Let $S$ be the set of limit points of $(p_{n+1}-p_n)/\log n$ sorry line 96 source
Source documentation
Let $S$ be the set of limit points of $(p_{n+1}-p_n)/\log n$. This problem asks whether $S=[0,\infty]$.
Since $\infty\in S$ is known (see erdos_5.variants.westzynthius), the open content is the equality of the finite part of $S$ with $[0,\infty)$.

depends on sorry what this means
Statement uses: Iff, True, Eq, Set, Real, Erdos5.limitPointSet, Set.Ici, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
7 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_5.variants.limit_point_set : answer(sorry) ↔ limitPointSet = Ici 0 := by
…
```
Mentions: Erdos5.limitPointSet
theorem Erdos5.erdos_5.variants.westzynthius $\infty\in S$ by Westzynthius' result [We31] on large prime gaps sorry line 103 source
Source documentation
$\infty\in S$ by Westzynthius' result [We31] on large prime gaps.

depends on sorry what this means
Statement uses: Exists, Nat, And, StrictMono, Filter.Tendsto, Real, Erdos5.normalizedGap, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_5.variants.westzynthius :
    ∃ n : ℕ → ℕ, StrictMono n ∧ Tendsto (fun i => normalizedGap (n i)) atTop atTop := by
…
```
Mentions: Erdos5.normalizedGap
theorem Erdos5.erdos_5.variants.goldston_pintz_yildirim $0\in S$ by the work of Goldston, Pintz, and Yildirim [GPY09] on small prime gaps sorry line 111 source
Source documentation
$0\in S$ by the work of Goldston, Pintz, and Yildirim [GPY09] on small prime gaps.

depends on sorry what this means
Statement uses: Membership.mem, Real, Set, Erdos5.limitPointSet, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
7 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_5.variants.goldston_pintz_yildirim : (0 : ℝ) ∈ limitPointSet := by
…
```
Mentions: Erdos5.limitPointSet
theorem Erdos5.erdos_5.variants.erdos_ricci Erdős [Er55] and Ricci [Ri56] independently showed that $S$ has positive Lebesgue measure sorry line 118 source
Source documentation
Erdős [Er55] and Ricci [Ri56] independently showed that $S$ has positive Lebesgue measure.

depends on sorry what this means
Statement uses: LT.lt, ENNReal, OfNat.ofNat, MeasureTheory.Measure, Real, Set, MeasureTheory.MeasureSpace.volume, Erdos5.limitPointSet
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_5.variants.erdos_ricci : 0 < volume limitPointSet := by
…
```
Mentions: Erdos5.limitPointSet
theorem Erdos5.erdos_5.variants.hildebrand_maier Hildebrand and Maier [HiMa88] showed that $S$ contains arbitrarily large (finite) numbers sorry line 125 source
Source documentation
Hildebrand and Maier [HiMa88] showed that $S$ contains arbitrarily large (finite) numbers.

depends on sorry what this means
Statement uses: Real, Exists, And, Membership.mem, Set, Erdos5.limitPointSet, LT.lt
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_5.variants.hildebrand_maier : ∀ C : ℝ, ∃ x ∈ limitPointSet, C < x := by
…
```
Mentions: Erdos5.limitPointSet
theorem Erdos5.erdos_5.variants.hildebrand_maier_measure [HiMa88] in fact prove the stronger statement that there is a constant $c>0$ with $\lambda([0,T]\cap S)\geq cT$ for all sufficiently large $T$ sorry line 133 source
Source documentation
[HiMa88] in fact prove the stronger statement that there is a constant $c>0$ with $\lambda([0,T]\cap S)\geq cT$ for all sufficiently large $T$.

depends on sorry what this means
Statement uses: Exists, Real, And, GT.gt, OfNat.ofNat, Filter.Eventually, LE.le, ENNReal, ENNReal.ofReal, HMul.hMul, MeasureTheory.Measure, Set, MeasureTheory.MeasureSpace.volume, Inter.inter, Erdos5.limitPointSet, Set.Icc, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
25 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_5.variants.hildebrand_maier_measure : ∃ c > (0 : ℝ), ∀ᶠ T : ℝ in atTop,
    ENNReal.ofReal (c * T) ≤ volume (limitPointSet ∩ Icc 0 T) := by
…
```
Mentions: c, Erdos5.limitPointSet
theorem Erdos5.erdos_5.variants.pintz Pintz [Pi16] showed that there exists some small constant $c>0$ such that $[0,c]\subset S$ sorry line 141 source
Source documentation
Pintz [Pi16] showed that there exists some small constant $c>0$ such that $[0,c]\subset S$.

depends on sorry what this means
Statement uses: Exists, Real, And, GT.gt, OfNat.ofNat, LE.le, Set, Set.Icc, Erdos5.limitPointSet
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_5.variants.pintz : ∃ c > (0 : ℝ), Icc 0 c ⊆ limitPointSet := by
…
```
Mentions: c, Erdos5.limitPointSet
theorem Erdos5.erdos_5.variants.banks_freiberg_maynard Banks, Freiberg, and Maynard [BFM16] showed that at least $12.5\%$ of $[0,\infty)$ belongs to $S$ sorry line 153 source
Source documentation
Banks, Freiberg, and Maynard [BFM16] showed that at least $12.5\%$ of $[0,\infty)$ belongs to $S$.
This is [BFM16, Theorem 1.1]: for any nine nonnegative reals $\beta_1\leq\beta_2\leq\cdots\leq\beta_9$, at least one of the differences $\beta_j-\beta_i$ with $i<j$ belongs to $S$.

depends on sorry what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, LE.le, Monotone, Exists, And, LT.lt, Membership.mem, Set, Erdos5.limitPointSet, HSub.hSub
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_5.variants.banks_freiberg_maynard (β : Fin 9 → ℝ) (hβ : ∀ i, 0 ≤ β i)
    (hβmono : Monotone β) : ∃ i j, i < j ∧ β j - β i ∈ limitPointSet := by
…
```
Mentions: Erdos5.limitPointSet
theorem Erdos5.erdos_5.variants.banks_freiberg_maynard_measure The $12.5\%$ claim itself, as deduced in [BFM16, Corollary 1.2]: $\lambda([0,T]\cap S)\geq (1-o(1))T/8$ as $T\to\infty$ sorry line 165 source
Source documentation
The $12.5\%$ claim itself, as deduced in [BFM16, Corollary 1.2]: $\lambda([0,T]\cap S)\geq (1-o(1))T/8$ as $T\to\infty$.
Note that the constant $1/8$ is only attained asymptotically and ineffectively; the bound [BFM16] obtain for all $T>0$ is the weaker $\lambda([0,T]\cap S)>T/22$.

depends on sorry what this means
Statement uses: Real, GT.gt, OfNat.ofNat, Filter.Eventually, LE.le, ENNReal, ENNReal.ofReal, HDiv.hDiv, HMul.hMul, HSub.hSub, Nat, MeasureTheory.Measure, Set, MeasureTheory.MeasureSpace.volume, Inter.inter, Erdos5.limitPointSet, Set.Icc, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
48 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_5.variants.banks_freiberg_maynard_measure : ∀ ε > (0 : ℝ), ∀ᶠ T : ℝ in atTop,
    ENNReal.ofReal ((1 - ε) * T / 8) ≤ volume (limitPointSet ∩ Icc 0 T) := by
…
```
Mentions: Erdos5.limitPointSet
theorem Erdos5.erdos_5.variants.merikoski Merikoski [Me20] showed that at least $1/3$ of $[0,\infty)$ belongs to $S$ sorry line 177 source
Source documentation
Merikoski [Me20] showed that at least $1/3$ of $[0,\infty)$ belongs to $S$.
This is [Me20, Theorem 1]: for any reals $\beta_1\leq\beta_2\leq\beta_3\leq\beta_4$, at least one of the differences $\beta_j-\beta_i$ with $i<j$ belongs to $S$. Note that, in contrast with erdos_5.variants.banks_freiberg_maynard, the $\beta_i$ are not required to be nonnegative.

depends on sorry what this means
Statement uses: Fin, OfNat.ofNat, Nat, Real, Monotone, Exists, And, LT.lt, Membership.mem, Set, Erdos5.limitPointSet, HSub.hSub
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_5.variants.merikoski (β : Fin 4 → ℝ) (hβmono : Monotone β) :
    ∃ i j, i < j ∧ β j - β i ∈ limitPointSet := by
…
```
Mentions: Erdos5.limitPointSet
theorem Erdos5.erdos_5.variants.merikoski_measure The $1/3$ claim itself [Me20, Corollary 2]: $\lambda([0,T]\cap S)\geq T/3$ for all $T>0$ sorry line 187 source
Source documentation
The $1/3$ claim itself [Me20, Corollary 2]: $\lambda([0,T]\cap S)\geq T/3$ for all $T>0$.
Unlike the $1/8$ of [BFM16], this bound holds uniformly in $T$ with no error term.

depends on sorry what this means
Statement uses: Real, GT.gt, OfNat.ofNat, LE.le, ENNReal, ENNReal.ofReal, HDiv.hDiv, Nat, MeasureTheory.Measure, Set, MeasureTheory.MeasureSpace.volume, Inter.inter, Erdos5.limitPointSet, Set.Icc
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
36 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_5.variants.merikoski_measure : ∀ T > (0 : ℝ),
    ENNReal.ofReal (T / 3) ≤ volume (limitPointSet ∩ Icc 0 T) := by
…
```
Mentions: Erdos5.limitPointSet
theorem Erdos5.erdos_5.variants.merikoski_bounded_gaps Merikoski [Me20] showed that $S$ has bounded gaps sorry line 198 source
Source documentation
Merikoski [Me20] showed that $S$ has bounded gaps.
This is [Me20, Corollary 3]: there is a (ineffective) constant $C\geq 0$ such that $S\cap[T,T+C]\neq\emptyset$ for all $T\geq 0$.

depends on sorry what this means
Statement uses: Exists, Real, And, GE.ge, OfNat.ofNat, Set.Nonempty, Inter.inter, Set, Erdos5.limitPointSet, Set.Icc, HAdd.hAdd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_5.variants.merikoski_bounded_gaps :
    ∃ C ≥ (0 : ℝ), ∀ T ≥ (0 : ℝ), (limitPointSet ∩ Icc T (T + C)).Nonempty := by
…
```
Mentions: Erdos5.limitPointSet
theorem Erdos5.erdos_5.variants.dense In [Er65b], [Er85c], and [Er97c] Erdős asks whether sorry line 207 source
Source documentation
In [Er65b], [Er85c], and [Er97c] Erdős asks whether $S$ is everywhere dense (but Weisenberg notes that clearly $S$ is closed so this is equivalent to asking whether $S=[0,\infty]$).

depends on sorry what this means
Statement uses: Iff, True, LE.le, Set, Real, Set.Ici, OfNat.ofNat, closure, Erdos5.limitPointSet
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_5.variants.dense : answer(sorry) ↔ Ici (0 : ℝ) ⊆ closure limitPointSet := by
…
```
Mentions: Erdos5.limitPointSet
theorem Erdos5.mem_limitPointSet_iff Membership in limitPointSet is exactly the existence of an infinite sequence of indices along which the normalised prime gaps converge, as in the statement of erdos_5 line 215 source
Source documentation
Membership in limitPointSet is exactly the existence of an infinite sequence of indices along which the normalised prime gaps converge, as in the statement of erdos_5.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Iff, Membership.mem, Set, Erdos5.limitPointSet, Exists, Nat, And, StrictMono, Filter.Tendsto, Erdos5.normalizedGap, Filter.atTop, nhds
Proof uses: Iff.intro, MapClusterPt.tendsto_subseq, MapClusterPt.of_comp, StrictMono.tendsto_atTop, Filter.Tendsto.mapClusterPt
27 instances, coercions and auxiliary constants left out.
```
theorem mem_limitPointSet_iff (x : ℝ) : x ∈ limitPointSet ↔
    ∃ n : ℕ → ℕ, StrictMono n ∧ Tendsto (fun i => normalizedGap (n i)) atTop (𝓝 x) :=
…
```
Mentions: Erdos5.limitPointSet, Erdos5.normalizedGap
theorem Erdos5.normalizedGap_nonneg The normalised prime gaps are nonnegative line 221 source
Source documentation
The normalised prime gaps are nonnegative.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Real, OfNat.ofNat, Erdos5.normalizedGap
Proof uses: div_nonneg, primeGap, Real.log, Nat.cast_nonneg, Real.log_natCast_nonneg
20 instances, coercions and auxiliary constants left out.
```
theorem normalizedGap_nonneg (n : ℕ) : 0 ≤ normalizedGap n :=
…
```
Mentions: Erdos5.normalizedGap
theorem Erdos5.limitPointSet_subset_Ici Every limit point of the normalised prime gaps is nonnegative line 226 source
Source documentation
Every limit point of the normalised prime gaps is nonnegative.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: LE.le, Set, Real, Erdos5.limitPointSet, Set.Ici, OfNat.ofNat
Proof uses: Membership.mem, Nat, And, StrictMono, Filter.Tendsto, Erdos5.normalizedGap, Filter.atTop, nhds, Exists, Iff.mp, Erdos5.mem_limitPointSet_iff, ge_of_tendsto', Erdos5.normalizedGap_nonneg
31 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem limitPointSet_subset_Ici : limitPointSet ⊆ Ici 0 := by
…
```
Mentions: Erdos5.limitPointSet
theorem Erdos5.erdos_5_iff_limit_point_set Documented declaration: erdos_5_iff_limit_point_set line 237 source
Source documentation
The statement of erdos_5 is equivalent to the description of the set of limit points in erdos_5.variants.limit_point_set; combine with mem_limitPointSet_iff to unfold the membership into the sequence of indices $n_i$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Iff, Real, LE.le, OfNat.ofNat, Membership.mem, Set, Erdos5.limitPointSet, Eq, Set.Ici
Proof uses: Iff.intro, LE.le.antisymm, Erdos5.limitPointSet_subset_Ici, Eq.rec, Eq.symm
15 instances, coercions and auxiliary constants left out.
```
theorem erdos_5_iff_limit_point_set :
    (∀ C : ℝ, 0 ≤ C → C ∈ limitPointSet) ↔ limitPointSet = Ici 0 :=
…
```
Mentions: Erdos5.limitPointSet
theorem Erdos5.isClosed_limitPointSet Documented declaration: isClosed_limitPointSet line 247 source
Source documentation
The set $S$ of limit points is closed, as Weisenberg notes in the acknowledgements to erdosproblems.com/5; consequently erdos_5.variants.dense and erdos_5.variants.limit_point_set ask the same question.

L4DEL explanation
The set $S$ of limit points is closed, as Weisenberg notes in the acknowledgements to erdosproblems.com/5; consequently erdos_5.variants.dense and erdos_5.variants.limit_point_set ask the same question.
Sources and attribution: Pinned Lean source (1646ca16afd6)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsClosed, Real, Erdos5.limitPointSet
Proof uses: isClosed_setOfPred_clusterPt, Filter.map, Nat, Erdos5.normalizedGap, Filter.atTop
7 instances, coercions and auxiliary constants left out.
```
theorem isClosed_limitPointSet : IsClosed limitPointSet := isClosed_setOfPred_clusterPt
…
```
Mentions: Erdos5.limitPointSet
theorem Erdos5.dense_iff_limit_point_set Weisenberg's remark, as reported on erdosproblems.com/5: since line 256 source
Source documentation
Weisenberg's remark, as reported on erdosproblems.com/5: since $S$ is closed, asking that $S$ be everywhere dense in $[0,\infty)$ is the same as asking that $S=[0,\infty)$, so erdos_5.variants.dense and erdos_5.variants.limit_point_set pose the same question.

L4DEL explanation
Weisenberg's remark, as reported on erdosproblems.com/5: since $S$ is closed, asking that $S$ be everywhere dense in $[0,\infty)$ is the same as asking that $S=[0,\infty)$, so erdos_5.variants.dense and erdos_5.variants.limit_point_set pose the same question.
Sources and attribution: Pinned Lean source (1646ca16afd6)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Iff, LE.le, Set, Real, Set.Ici, OfNat.ofNat, closure, Erdos5.limitPointSet, Eq
Proof uses: Eq.mpr, id, congrArg, IsClosed.closure_eq, Erdos5.isClosed_limitPointSet, Iff.intro, LE.le.antisymm, Erdos5.limitPointSet_subset_Ici, Eq.ge
20 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem dense_iff_limit_point_set :
    Ici (0 : ℝ) ⊆ closure limitPointSet ↔ limitPointSet = Ici 0 := by
…
```
Mentions: Erdos5.limitPointSet