TheoremStatement: 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.

The closure equals the set together with its limit points, equals the set of points every neighbourhood of which meets it, and is the smallest closed superset; a set is closed iff it contains its limit points

Statement

Let $A \subseteq R$ , with closure $\overline{A}$ as in Interior, closure, boundary and exterior of a subset of $R$ and derived set $A^{'}$ as in Limit point, isolated point, adherent point, derived set, and dense subset of $R$ . Write

$E : = {x \in R : N_{ε} (x) \cap A \neq \emptyset for every real ε > 0}$

for the set of adherent points of $A$ (The $ε$ -neighbourhood and the punctured $ε$ -neighbourhood of a point of $R$ ). Then:

$\overline{A} = E$ .
$\overline{A} = A \cup A^{'}$ .
$\overline{A}$ is the smallest closed superset of $A$ : it is closed, it contains $A$ , and it is contained in every closed $F$ with $A \subseteq F$ .
$A$ is closed if and only if $A = \overline{A}$ , if and only if $A^{'} \subseteq A$ .

Claim 3 is the content of the definition of $\overline{A}$ and is restated here so that the four descriptions stand together; claims 1, 2 and 4 are the ones that carry work.

Facts & Assumptions

Given: A subset $A \subseteq R$ , and the set $E$ of adherent points of $A$ as displayed in the Statement.

[L1]

$U$ is open when every $x \in U$ admits $ε > 0$ with $N_{ε} (x) \subseteq U$ ; $F$ is closed when $R ∖ F$ is open (Open subset of $R$ (every point has a neighbourhood inside it), closed subset (complement open), and clopen).

[L2]

$x \in N_{ε} (x)$ ; $N_{ε}^{*} (x) = N_{ε} (x) ∖ {x} \subseteq N_{ε} (x)$ ; and if $y \in N_{ε} (x)$ then $δ : = ε - ∣ y - x ∣ > 0$ and $N_{δ} (y) \subseteq N_{ε} (x)$ (The $ε$ -neighbourhood and the punctured $ε$ -neighbourhood of a point of $R$ ).

[L3]

$\overline{A}$ is the intersection of the nonempty family of closed supersets of $A$ ; it is closed, it contains $A$ , and it is contained in every closed superset of $A$ (Interior, closure, boundary and exterior of a subset of $R$ , Arbitrary unions and finite intersections of open subsets of $R$ are open, and dually for closed sets).

[L4]

$x$ is an adherent point of $A$ when every $N_{ε} (x)$ meets $A$ , a limit point when every $N_{ε}^{*} (x)$ meets $A$ , and $A^{'}$ is the set of limit points (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ).

Proof

technique · direct

1.1

$A \subseteq E$ : for $x \in A$ and any $ε > 0$ one has $x \in N_{ε} (x) \cap A$ , so that intersection is nonempty.

L2L4

1.2

Let $x \in R ∖ E$ ; by the definition of $E$ there is a real $ε > 0$ with $N_{ε} (x) \cap A = \emptyset$ .

L4choose

1.3

Let $F$ be closed with $A \subseteq F$ , and let $x \in R ∖ F$ ; since $R ∖ F$ is open there is a real $η > 0$ with $N_{η} (x) \subseteq R ∖ F$ .

L1choose

2.1

For every $y \in N_{ε} (x)$ the radius $δ : = ε - ∣ y - x ∣$ is positive and $N_{δ} (y) \subseteq N_{ε} (x)$ , so $N_{δ} (y) \cap A = \emptyset$ and $y \notin E$ ; hence $N_{ε} (x) \subseteq R ∖ E$ , and since $x$ was an arbitrary point of $R ∖ E$ that set is open, that is, $E$ is closed.

step 1.2L1L2L4

2.2

From $N_{η} (x) \subseteq R ∖ F \subseteq R ∖ A$ we get $N_{η} (x) \cap A = \emptyset$ , so $x \notin E$ ; hence $R ∖ F \subseteq R ∖ E$ , that is, $E \subseteq F$ , for every closed $F \supseteq A$ .

step 1.3L4

3.1

By steps 1.1 and 2.1 the set $E$ is a closed superset of $A$ , so $\overline{A} \subseteq E$ by the leastness in [L3]; and $\overline{A}$ is itself a closed superset of $A$ by [L3], so step 2.2 applied to $F = \overline{A}$ gives $E \subseteq \overline{A}$ . Hence $\overline{A} = E$ , which is claim 1.

step 1.1step 2.1step 2.2L3

4.1

$E = A \cup A^{'}$ : if $x \in E$ and $x \notin A$ then for every $ε > 0$ some $a \in N_{ε} (x) \cap A$ exists, and $a \neq x$ because $x \notin A$ , so $a \in N_{ε}^{*} (x) \cap A$ and $x \in A^{'}$ ; conversely $A \subseteq E$ by step 1.1, and $A^{'} \subseteq E$ because $N_{ε}^{*} (x) \subseteq N_{ε} (x)$ . Combining with step 3.1 gives $\overline{A} = A \cup A^{'}$ , which is claim 2.

step 1.1step 3.1L2L4

5.1

Claim 4: if $A$ is closed then $A$ is a closed superset of itself, so $\overline{A} \subseteq A$ by [L3], while $A \subseteq \overline{A}$ by [L3], whence $A = \overline{A}$ ; conversely if $A = \overline{A}$ then $A$ is closed because $\overline{A}$ is. Finally $A = \overline{A}$ says $A = A \cup A^{'}$ by step 4.1, and $A = A \cup A^{'}$ holds exactly when $A^{'} \subseteq A$ .

step 4.1L3

6.1

Claim 3 is [L3] restated, and claims 1, 2 and 4 are steps 3.1, 4.1 and 5.1, so all four hold.

step 3.1step 4.1step 5.1L3∎

Remarks

Which claim does the work in practice. Claim 1 is the one used almost everywhere below: to show a point lies in $\overline{A}$ one exhibits, for each $ε > 0$ , a point of $A$ within $ε$ of it. Claim 2 is what separates the two ways a point can be adherent, by membership or by accumulation, and it is what makes the notion of an isolated point visible.
No special property of $R$ is used. The argument uses the definitions of open, closed, neighbourhood and closure, and the order enters only through the nesting property of neighbourhoods; neither the least-upper-bound property nor the Archimedean property appears at any step. The results of this page that do use them are flagged in Which results on this page use the order of $R$ and therefore have no general-topological analogue.
The sequential form is a separate theorem and costs more. Replacing "every neighbourhood meets $A$ " by "some sequence in $A$ converges to $x$ " is A point lies in the closure of $A \subseteq R$ iff some sequence in $A$ converges to it, so a subset of $R$ is closed iff it is sequentially closed, and the passage from the first to the second spends the axiom of countable choice, since it selects one point of $A$ from each of infinitely many neighbourhoods. The characterisation proved above is choice free.

Depends on

Used by

…and 1 more result.

Dependency tree · two levels

14 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

Closure (topology) (Wikipedia) (standard reference, not scraped)
Limit point (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 2 (Thm 2.27) (standard reference, not scraped)
J. Lebl, Basic Analysis I, §7.2 (standard reference, not scraped)
J. K. Hunter, An Introduction to Real Analysis (standard reference, not scraped)