Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-29 (claude-fable-5)
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.

A space is locally connected exactly when every component of every open subspace is open; in that case the components of the space itself are clopen

Statement

Let X be a topological space, with subsets carrying the subspace topology (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace). Then:

  1. X is locally connected (Locally connected and locally path-connected spaces: a neighbourhood base of open connected, respectively open path-connected, sets at every point) if and only if for every open U⊆X every component of the space U (Connected components, quasicomponents, and totally disconnected spaces) is open in X.
  2. If X is locally connected then every component of X is clopen.
  3. The same statement with "path-connected" throughout: X is locally path-connected if and only if for every open U⊆X every path component of the space U is open in X.

In claim 1 "open in X" and "open in U" say the same thing, U being open in X (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace); the statement is written with the ambient form because that is how it is used.

Facts & Assumptions

Given: A topological space X; for open U⊆X and x∈U, write CU(x) for the component and PU(x) for the path component of x in the space U.

[A1]

X is locally connected at x when every open U∋x contains an open connected V with x∈V⊆U; locally path-connected likewise with "path-connected" (Locally connected and locally path-connected spaces: a neighbourhood base of open connected, respectively open path-connected, sets at every point).

[A2]

CU(x) is the largest connected subset of U containing x: it is connected, contains x, and contains every connected A⊆U with x∈A (Connected components, quasicomponents, and totally disconnected spaces, Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets). The same holds for PU(x) with "path-connected" in place of "connected": the path components are the classes of the joined-by-a-path equivalence relation, each path-connected and containing its point (Paths, path-connected spaces and path components).

[A4]

A set is open exactly when it is a neighbourhood of each of its points, equivalently when each of its points has an open set around it inside it; and a union of open sets is open (Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open, Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

Proof

technique · direct
1.1

Assume X is locally connected, let U⊆X be open, let C be a component of the space U and let x∈C; then C=CU(x) by [A2], components being determined by any of their points.

A1A2
1.2

Conversely assume every component of every open subspace is open in X, and let x∈U with U open; put V:=CU(x).

A2
2.1

In the situation of step 1.1, [A1] supplies an open connected V with x∈V⊆U; V is then a connected subset of U containing x, so V⊆CU(x)=C by [A2].

step 1.1A1A2
2.2

In the situation of step 1.2, V is connected and contains x by [A2], it is contained in U, and it is open in X by hypothesis; so x∈V⊆U with V open and connected.

step 1.2A2
3.1

So in the situation of step 1.1 every point of C has an open set around it inside C, whence C is open in X by [A4]. This is the forward implication of claim 1.

step 1.1step 2.1A4
3.2

And step 2.2 is exactly the condition of [A1] at x, so X is locally connected; this is the backward implication, and claim 1 follows.

step 2.2A1
4.1

For claim 2, let C be a component of X; taking U=X, which is open, claim 1 makes C open in X, and [A5] makes it closed, so C is clopen.

step 3.1step 3.2A3A5
5.1

For claim 3, replace "connected" by "path-connected" and CU by PU throughout steps 1.1, 1.2, 2.1, 2.2, 3.1 and 3.2: every property of CU used there is recorded for PU in [A2], namely that it contains its point, is path-connected, and contains every path-connected subset of U through that point, the last because two points joined to x are joined to each other.

step 3.1step 3.2A1A2A4∎

Remarks

  • Why the criterion is stated for every open subspace and not only for X. Openness of the components of X alone is strictly weaker: a space may have a single component, itself, which is trivially open, while failing to be locally connected at some point. The strength of local connectedness is that the conclusion holds inside every open piece, however small, and that is what the proof of the forward implication uses at step 2.1 — it applies the hypothesis inside the given U, not inside X.

  • Claim 2 is the practical form. Once the components are clopen, a connectedness argument reduces to counting them: a locally connected space is connected exactly when it has one component, and the components behave like the summands of a disjoint union.

  • What claim 2 does not say. It does not say that a space whose components are clopen is locally connected, and that converse is false in general. Nor does the theorem assert any implication between connectedness and local connectedness; those are settled separately on this page.

Depends on

Used by

Dependency tree · two levels

24 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