DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-08-02

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.

Compatible normal sequences of open covers

Definition

For an open cover $U$ and $x \in X$ , write $St (x, U) = St ({x}, U)$ , using the star of Refinements, locally finite families, point-finite families, and star refinements. A sequence $(U_{n})_{n \in N}$ of open covers is normal if $U_{n + 1}$ star-refines $U_{n}$ for every $n$ .

It is compatible with the topology if (i) for $x \neq y$ some $n$ has $y \notin St (x, U_{n})$ , and (ii) for every open neighbourhood $O$ of $x$ (Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open) some $n$ has $St (x, U_{n}) \subseteq O$ . The indexing starts at $0$ ; an empty space has the legal empty cover at every index.

Depends on

Used by

A T₁ space with a compatible normal sequence of open covers is metrizable Lemma

Dependency tree · two levels

5 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

Umeå University, The Smirnov- and Bing–Nagata–Smirnov Metrization Theorems (standard reference, not scraped)