Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-29 (claude-fable-5)
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.

Two continuous maps into a Hausdorff space that agree on a dense subset are equal

Statement

Let Z be a topological space, let D⊆Z be dense (Dense, nowhere dense and codense subsets of a topological space, and the criterion by basic open sets), let Y be Hausdorff (Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not) and let f,g:Z→Y be continuous (Continuity of a map of topological spaces at a point and globally) with

f(d)=g(d)for every d∈D.

Then f=g.

So a continuous map into a Hausdorff space is determined by its restriction to any dense subset of its domain. Nothing is asserted about which functions on D extend: the statement is about uniqueness of an extension, not existence.

Facts & Assumptions

Proof

technique · direct
1.1

E(f,g) is closed in Z.

L1
1.2

D⊆E(f,g), since f and g agree at every point of D.

given
2.1

Z=D‾⊆E(f,g), the equality by [A1] and the inclusion because E(f,g) is a closed set containing D.

step 1.1step 1.2A1L2
3.1

E(f,g)⊆Z holds by definition, so E(f,g)=Z, that is f(z)=g(z) for every z∈Z and f=g.

step 2.1∎

Remarks

  • The Hausdorff hypothesis is spent exactly once, inside [L1], and the density hypothesis exactly once, at step 2.1. Neither is used anywhere else, and neither can be weakened to the other: a dense agreement set alone does not force equality without a separation hypothesis on the codomain, and a Hausdorff codomain alone plainly does not.

  • Density is a hypothesis about Z, not about Y. In particular the statement is about one domain and one dense subset of it; it says nothing about restrictions to subsets that are merely large in some other sense, and there is no cardinality condition anywhere in it.

  • The uniqueness/existence split matters. A continuous f:D→Y need not extend continuously to Z at all. What this corollary rules out is two different extensions, and that is exactly what makes an extension, when it exists, worth naming.

Depends on

Used by

Dependency tree · two levels

18 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