LemmaStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedprecheck pass

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 closed discrete subset of a compact space is finite

Statement

Let $X$ be a compact topological space (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right) and let $S \subseteq X$ be closed and discrete, meaning that for every $s \in S$ there is an open $U_{s} \subseteq X$ with $U_{s} \cap S = {s}$ (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, Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison). Then $S$ is finite.

Facts & Assumptions

Given: A compact topological space $X$ and a closed subset $S \subseteq X$ such that for every $s \in S$ there is an open set $U \subseteq X$ with $U \cap S = {s}$ .

[F1]

Every open cover of a compact space has a finite subcover, possibly empty when $X = \emptyset$ ; a nonempty finite subcover can be listed as $U_{0}, \dots, U_{n}$ with $X = U_{0} \cup \dots \cup U_{n}$ (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).

[F2]

A subset $S \subseteq X$ is closed exactly when $X ∖ S$ is open (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

Proof

1.1givenF2

By [F2] the complement $X ∖ S$ is open; form the family $U : = {X ∖ S} \cup {U \subseteq X open : U \cap S is a singleton}$ , a set of open subsets of $X$ defined by comprehension, so forming it selects nothing. It is an open cover of $X$ : a point $x \notin S$ lies in $X ∖ S$ , and a point $s \in S$ lies in some open $U$ with $U \cap S = {s}$ by the hypothesis, and this $U$ is a member of $U$ .

2.1step 1.1F1∎

By [F1] the cover $U$ has a finite subcover. If it is empty, then $X = \emptyset$ and $S = \emptyset$ is finite. Otherwise list it as $U_{0}, \dots, U_{n}$ . Each $U_{i}$ is $X ∖ S$ or open with $U_{i} \cap S = {s_{i}}$ a singleton, and $X ∖ S$ meets $S$ in nothing. Intersecting the covering relation $X = U_{0} \cup \dots \cup U_{n}$ with $S$ gives $S \subseteq {s_{i} : U_{i} \cap S is a singleton}$ , a finite set, so by the listing form of finiteness (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right) the set $S$ is finite; if no $U_{i}$ has a singleton trace then $S \subseteq \emptyset$ , so $S = \emptyset$ and $S$ is finite as well.

Depends on

Used by

Dependency tree · two levels

10 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

Victor Guillemin and Alan Pollack, Differential Topology (Prentice-Hall 1974; complete 236-page PDF) (standard reference, not scraped)
Peter Wong, Lectures on Fixed Point Theory, Mini-Course XV Encontro Brasileiro de Topologia, Rio Claro 2006 (complete notes) (standard reference, not scraped)