LemmaStatement: AI-adaptedProof: AI-generatedSession-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.

A countable local base can be chosen open and decreasing

Statement

If $X$ is first countable and $x\in X$ , then $x$ has a countable local base $(V_n)_{n\in\mathbb N}$ of open sets with $V_{n+1}\subseteq V_n$ .

Facts & Assumptions

Given: A countable local base at $x$ (First countable space: a countable neighbourhood base at every point).

[L1]

Each neighbourhood of $x$ contains an open neighbourhood of $x$ (Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open).

[L2]

Every nonempty at most countable set is a surjective image of $\mathbb N$ (A nonempty set is at most countable iff it is a surjective image of $\mathbb{N}$ , Finite, countably infinite, countable, uncountable).

Proof

technique · constructive

1.1

A local base is nonempty, so enumerate it as $(B_n)$ by [L2], with repetitions allowed. Put $U_n=\operatorname{int}(B_n)$ . Since $B_n$ is a neighbourhood of $x$ , its interior is open, contains $x$ , and is contained in $B_n$ . This definition is canonical and uses no countable choice.

givenL1L2construct

2.1

Put $V_n=U_0\cap\cdots\cap U_n$ ; each $V_n$ is open, contains $x$ , and $V_{n+1}\subseteq V_n$ .

step 1.1construct

3.1

Since $V_n\subseteq B_n$ , every neighbourhood contains some $V_n$ , so $(V_n)$ is the required decreasing local base.

step 2.1discharge-construct∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 39 results over 16 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

UCR General Topology Notes (standard reference, not scraped)
First-countable space (Wikipedia) (standard reference, not scraped)