Topological Spaces and Continuity

About this page

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.

✓ 13 results · all verified · 10 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 3 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

1 · Prerequisites

Real Analysis

Set Theory

Topology

Metric Spaces

2 · Logical flowchart

3 · Items

Definition

A family is a basis for a unique topology iff it covers the set and every point of an intersection of two members lies in a member inside that intersection; finite intersections of any subbasis form a basis

Definition

Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open

Definition

Interior, closure, boundary, exterior, derived set and isolated point in a topological space

Theorem

A point lies in the closure of A iff every basic neighbourhood of it meets A; the closure is the smallest closed superset and equals A together with its derived set

Lemma

Interior commutes with finite intersections and closure with finite unions, while the two reverse combinations are inclusions only and both fail for infinite families; the space is the disjoint union of interior, boundary and exterior

Definition

Dense, nowhere dense and codense subsets of a topological space, and the criterion by basic open sets

Theorem

Kuratowski: operators satisfying c(∅) = ∅, A ⊆ c(A), c(c(A)) = c(A) and c(A ∪ B) = c(A) ∪ c(B) correspond bijectively to topologies

Definition

Continuity of a map of topological spaces at a point and globally

Theorem

For a map of spaces the following agree: continuity at every point, preimages of open sets open, preimages of closed sets closed, preimages of subbasic open sets open, and f(Ā) ⊆ f(A)

Definition

Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace

Lemma

Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous

Definition

Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological

Lemma

A continuous bijection is a homeomorphism iff it is open iff it is closed, and homeomorphy is an equivalence relation on spaces

Definition

Convergence and cluster points of a sequence in a topological space, sequential continuity, and the sequential closure

Lemma

The sequential closure is contained in the closure, continuity implies sequential continuity, and sequential limits need not be unique

Definition

First countable space: a countable neighbourhood base at every point

Theorem

Assuming Countable Choice, in a first countable space sequential closure equals closure and sequential continuity at a point equals continuity there

Definition

Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not

Remark

Topological Spaces and Continuity

3 · Items

Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison

The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies

Basis and subbasis for a topology, and the topology generated by a family of sets

A family is a basis for a unique topology iff it covers the set and every point of an intersection of two members lies in a member inside that intersection; finite intersections of any subbasis form a basis

Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open

Interior, closure, boundary, exterior, derived set and isolated point in a topological space

A point lies in the closure of A iff every basic neighbourhood of it meets A; the closure is the smallest closed superset and equals A together with its derived set

Interior commutes with finite intersections and closure with finite unions, while the two reverse combinations are inclusions only and both fail for infinite families; the space is the disjoint union of interior, boundary and exterior

Dense, nowhere dense and codense subsets of a topological space, and the criterion by basic open sets

Kuratowski: operators satisfying c(∅) = ∅, A ⊆ c(A), c(c(A)) = c(A) and c(A ∪ B) = c(A) ∪ c(B) correspond bijectively to topologies

Continuity of a map of topological spaces at a point and globally

For a map of spaces the following agree: continuity at every point, preimages of open sets open, preimages of closed sets closed, preimages of subbasic open sets open, and f(Ā) ⊆ f(A)

Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace

Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous

Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological

A continuous bijection is a homeomorphism iff it is open iff it is closed, and homeomorphy is an equivalence relation on spaces

Convergence and cluster points of a sequence in a topological space, sequential continuity, and the sequential closure

The sequential closure is contained in the closure, continuity implies sequential continuity, and sequential limits need not be unique

First countable space: a countable neighbourhood base at every point

Assuming Countable Choice, in a first countable space sequential closure equals closure and sequential continuity at a point equals continuity there

Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not

The four live convention forks of general topology and which side this library takes on each

FALSE: an arbitrary intersection of open sets is open in every topological space

FALSE: a sequentially continuous map between topological spaces is continuous

FALSE: every continuous bijection of topological spaces is a homeomorphism

FALSE: every topology is induced by some metric