TheoremStatement: Literature-sourcedProof: 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 map of topological spaces is continuous at a point if and only if it preserves every net converging to that point

Statement

Let $f:X\to Y$ and $p\in X$ . Then $f$ is continuous at $p$ if and only if, for every net $x_d\to p$ in $X$ , the net $f(x_d)$ converges to $f(p)$ in $Y$ .

Facts & Assumptions

Given: A function $f:X\to Y$ and a point $p\in X$ .

[A1]

$f$ is continuous at $p$ exactly when every neighbourhood $V$ of $f(p)$ has $f^{-1}[V]$ as a neighbourhood of $p$ (Continuity of a map of topological spaces at a point and globally).

[A2]

A point is in the closure of a set exactly when a net in that set converges to it (A point lies in the closure of a set if and only if a net in the set converges to it).

[A3]

A net converges exactly when it is eventually in every neighbourhood (Convergence and cluster points of a net in a topological space).

Proof

technique · contradiction

1.1

If $f$ is continuous at $p$ and $x_d\to p$ , then for every neighbourhood $V$ of $f(p)$ the net is eventually in $f^{-1}[V]$ by [A1], hence $f(x_d)$ is eventually in $V$ and converges to $f(p)$ .

A1A3

1.2

Conversely, assume every net converging to $p$ has image converging to $f(p)$ , and assume for a contradiction that $f$ is not continuous at $p$ . Then some neighbourhood $V$ of $f(p)$ has $f^{-1}[V]$ not a neighbourhood of $p$ .

A1assume-contra

2.1

Put $A=X\setminus f^{-1}[V]$ . Every neighbourhood of $p$ meets $A$ , for otherwise it would be contained in $f^{-1}[V]$ ; hence $p\in\overline A$ and [A2] gives a net $x_d$ in $A$ converging to $p$ .

step 1.2A2

3.1

Every $f(x_d)$ lies outside $V$ , so its image net is not eventually in the neighbourhood $V$ of $f(p)$ and cannot converge to $f(p)$ , contradicting the assumption of step 1.2.

step 2.1A3

4.1

Therefore $f$ is continuous at $p$ ; together with step 1.1 this proves the equivalence.

step 1.1step 3.1discharge-contradiction∎

Depends on

Used by

Dependency tree · next 3 levels

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

WVU Math 581 Topology I (standard reference, not scraped)
Net (mathematics) (Wikipedia) (standard reference, not scraped)