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.
Continuity of a map of topological spaces at a point and globally
Definition
Let and be topological spaces (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison), let be a function and let . Neighbourhoods are as in Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open.
is continuous at if for every neighbourhood of in the preimage is a neighbourhood of in .
is continuous if it is continuous at every point of .
The same condition with open sets only. is continuous at if and only if for every open with there is an open with and . Indeed, if is continuous at and is such an open set, then is a neighbourhood of , so is a neighbourhood of and contains an open , which satisfies . Conversely, given the displayed condition and a neighbourhood of , fix open with and then open with ; then , so is a neighbourhood of . Both forms are used below and are the same statement written twice.
Preimage, not image. is the preimage in the sense of Injection, surjection, bijection and is defined for every function, invertible or not; no inverse function is being asserted to exist. Continuity is a condition on preimages throughout, and the corresponding conditions on images define the open and closed maps of a later item, which are different notions.
Remarks
-
This is the metric definition when both topologies are metric topologies. For metric spaces, - continuity at (Continuity of a map between metric spaces, at a point and globally, in the - form) says that every ball around has a ball around mapped into it, and the balls around a point are a neighbourhood base there; the identification is carried out where metrizable spaces are defined later on this page. Nothing about a metric survives in the definition above: continuity is a relation between two topologies and a function, and it is meaningless to ask whether a function between bare sets is continuous.
-
Continuity depends on both topologies, and coarsening the target or refining the source only helps. If is continuous and is replaced by a finer topology, or by a coarser one, remains continuous, since each condition to be verified is weakened and each neighbourhood available in the source is still available. In particular every map out of a discrete space and every map into an indiscrete space is continuous (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies).
-
Continuity at a point is strictly weaker than continuity. A function may be continuous at exactly one point, and the definition above is deliberately local so that the sequential criteria proved later can be stated pointwise.