ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck 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.

The sequential fan is Fréchet–Urysohn and not first countable

Example

Let $S_{ω} = (N \times N) \cup {\infty}$ , with all $(n, m)$ isolated. A neighbourhood of $\infty$ contains $\infty$ and, for every $n$ , all but finitely many $(n, m)$ on the $n$ -th spoke. This is the sequential fan. It is Fréchet–Urysohn but not first countable.

Facts & Assumptions

Given: The sequential fan and a subset $A \subseteq S_{ω}$ .

[A1]

A space is Fréchet–Urysohn when closure points are limits of sequences from the set, and first countability means a countable local base (Fréchet–Urysohn spaces and sequential spaces, First countable space: a countable neighbourhood base at every point).

[L1]

Every nonempty finite subset of $N$ has a maximum, every nonempty subset of $N$ has a least member, and recursion defines sequences from uniquely specified successive terms (Every nonempty finite set of reals has a maximum and a minimum, The well-ordering principle, The recursion theorem).

Verification

technique · constructive

1.1

Suppose $\infty \in \overline{A}$ . If every spoke met $A$ only finitely, define $f (n) = {\begin{cases} 0, & {m : (n, m) \in A} = \emptyset, \\ 1 + \max {m : (n, m) \in A}, & otherwise . \end{cases}$ This is a canonically defined function by [L1], and the neighbourhood containing on spoke $n$ exactly the points $(n, m)$ with $m \geq f (n)$ misses $A$ , a contradiction. Hence one spoke meets $A$ infinitely.

A1L1construct

1.2

Suppose $(B_{k})$ were a countable neighbourhood base at $\infty$ . For each $k, n$ , let $f_{k} (n)$ be the least threshold such that $(n, m) \in B_{k}$ for every $m \geq f_{k} (n)$ ; it exists and is unique by [L1]. Form the neighbourhood whose threshold on spoke $k$ is $g (k) = f_{k} (k) + 1$ .

A1L1construct

2.1

On the infinite spoke supplied by step 1.1, recursion and least elements from [L1] list the second coordinates increasingly. The resulting sequence in $A$ is eventually beyond every threshold on that spoke, hence converges to $\infty$ . Isolated closure points already lie in $A$ , so $S_{ω}$ is Fréchet–Urysohn.

step 1.1A1L1

2.2

The point $(k, f_{k} (k))$ lies in $B_{k}$ but not in this neighbourhood, so no $B_{k}$ is contained in it. This contradicts the base property.

step 1.2A1

3.1

Therefore the sequential fan is Fréchet–Urysohn and not first countable.

step 2.1step 2.2discharge-construct∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

27 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

D. Ma, A note on products of sequential fans (Dan Ma's Topology Blog) (standard reference, not scraped)
Fréchet–Urysohn space (Wikipedia) (standard reference, not scraped)