LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31

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.

Locally finite families remain locally finite after taking closures, closure commutes with their union, and a locally finite union of closed sets is closed

Statement

Let $\{A_i\}_{i\in I}$ be a locally finite family of subsets of a topological space $X$ . Then $\{\overline{A_i}\}_{i\in I}$ is locally finite and $\overline{\bigcup_{i\in I}A_i}=\bigcup_{i\in I}\overline{A_i}.$ Consequently, a locally finite union of closed subsets of $X$ is closed.

Facts & Assumptions

Given: A locally finite family $\{A_i\}_{i\in I}$ in a topological space $X$ .

[F1]

Local finiteness says that each point has a neighbourhood meeting only finitely many $A_i$ (Refinements, locally finite families, point-finite families, and star refinements).

[L1]

A point belongs to $\overline A$ exactly when every neighbourhood of it meets $A$ , and $\overline A$ is the smallest closed superset of $A$ (A point lies in the closure of $A$ iff every basic neighbourhood of it meets $A$ ; the closure is the smallest closed superset and equals $A$ together with its derived set).

Proof

technique · direct

1.1

Fix $x\in X$ and a neighbourhood $N$ of $x$ meeting only $A_{i_1},\ldots,A_{i_n}$ . Choose an open neighbourhood $O$ of $x$ with $O\subseteq N$ . If $O\cap\overline{A_j}\ne\varnothing$ , choose $y\in O\cap\overline{A_j}$ ; the open neighbourhood $O$ of $y$ then meets $A_j$ , so $N$ meets $A_j$ and $j\in\{i_1,\ldots,i_n\}$ .

F1L1

1.2

The inclusion $\bigcup_i\overline{A_i}\subseteq\overline{\bigcup_iA_i}$ holds because each $\overline{A_i}$ is contained in every closed set containing $A_i$ , in particular in $\overline{\bigcup_iA_i}$ .

2.1

Thus $O$ meets only $\overline{A_{i_1}},\ldots,\overline{A_{i_n}}$ , so the closed family is locally finite.

step 1.1F1

2.2

Let $x\in\overline{\bigcup_iA_i}$ and take $N$ as in step 1.1; if $x\notin\bigcup_i\overline{A_i}$ , then for each $i_k$ an open neighbourhood of $x$ misses $A_{i_k}$ , and its finite intersection with an open neighbourhood inside $N$ misses every $A_i$ , contradicting the closure criterion.

step 1.1L1

3.1

Hence $\overline{\bigcup_iA_i}=\bigcup_i\overline{A_i}$ by steps 1.2 and 2.2; if every $A_i$ is closed, the right-hand side is $\bigcup_iA_i$ , so that union is closed.

step 1.2step 2.2L1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 12 results over 6 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

J. Robbin, Partitions of Unity (standard reference, not scraped)
S. Semmes, Topology notes, Sections 5.13–5.14 (Rice University) (standard reference, not scraped)