DefinitionDefinition: AI-adaptedProof: Not applicableSession-authored (Fable 5 assisted)audited 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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 10 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

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