Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Both Q and R∖Q are dense in R, and every nonempty open subset of R is uncountable

Statement

Write QR for the image of Q in R under the canonical embedding q↦q^ (The rationals embed densely in the reals), the set usually written Q once the identification is made, and put X:=R∖QR for the irrationals. Then:

  1. QR is dense in R, that is, QR‾=R (Limit point, isolated point, adherent point, derived set, and dense subset of R);
  2. X is dense in R;
  3. every nonempty open subset of R is uncountable (Finite, countably infinite, countable, uncountable).

Claim 2 is not a symmetry of claim 1: the rationals are dense because they are constructed to approximate, whereas the irrationals are dense because there are too many points in any interval for a countable set to exhaust it, which is why claim 3 is proved alongside and used for it.

Facts & Assumptions

Given: The canonical embedding q↦q^ of Q into R, its image QR, and the complement X=R∖QR.

[L2]
[L3]

U is open when every x∈U admits ε>0 with Nε(x)⊆U (Open subset of R (every point has a neighbourhood inside it), closed subset (complement open), and clopen).

[L4]

Strictly between any two reals lies an element of QR, and q↦q^ is injective (The rationals embed densely in the reals).

[L5]

Q≈N (Q is countably infinite); an injection is a bijection onto its image, and ≈ is symmetric and transitive (Injection, surjection, bijection, Equinumerous sets, A≈B and A⪯B).

[L6]

Every subset of an at most countable set is at most countable, and uncountable means not at most countable (Every subset of an at most countable set is at most countable, Finite, countably infinite, countable, uncountable).

[L7]

For a<b the interval (a,b) is uncountable (Every nondegenerate interval of R is uncountable).

Proof

technique · direct
1.1

QR is dense: let x∈R and let ε>0 be real; by [L2] one has x−ε<x+ε, so [L4] supplies q^ with x−ε<q^<x+ε, that is q^∈Nε(x)∩QR. Every real is therefore an adherent point of QR and claim 1 follows from [L1].

L1L2L4
1.2

QR is at most countable: the embedding is an injection of Q with image QR, hence a bijection onto it, so QR≈Q≈N.

L4L5
1.3

For all reals a<b the interval (a,b) is uncountable.

L7
2.1

For all reals a<b the interval (a,b) contains an irrational: if it did not, then (a,b)⊆QR, so (a,b) would be a subset of an at most countable set by step 1.2 and hence at most countable by [L6], contradicting step 1.3. So some z∈(a,b) lies in X.

step 1.2step 1.3L6
2.2

Every nonempty open U⊆R is uncountable: fix x∈U and, by [L3], a real ε>0 with Nε(x)⊆U; by [L2] the set Nε(x) is the interval (x−ε,x+ε) with x−ε<x+ε, hence uncountable by step 1.3. Were U at most countable, its subset Nε(x) would be at most countable by [L6], which it is not; so U is uncountable, which is claim 3.

step 1.3L2L3L6choose
3.1

X is dense: let x∈R and let ε>0 be real; applying step 2.1 with a=x−ε and b=x+ε gives z∈(x−ε,x+ε)∩X, which is Nε(x)∩X by [L2]. Every real is therefore an adherent point of X, so X‾=R by [L1], which is claim 2.

step 2.1L1L2
4.1

Claims 1, 2 and 3 are steps 1.1, 3.1 and 2.2, so both QR and its complement are dense in R and every nonempty open subset of R is uncountable.

step 1.1step 2.2step 3.1∎

Remarks

Depends on

Used by

…and 36 more results.

Dependency tree · two levels

63 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources