Alphabeta Math

Metric Spaces

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.

✓ 18 results · all verified · 12 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 6 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.
1 · Prerequisites
Real Analysis
Set Theory
2 · Logical flowchart

3 · Items

Definition

Metric space: d(x,y) = 0 iff x = y, symmetry, and the triangle inequality; pseudometric and ultrametric

Lemma

Nonnegativity of a metric is a consequence of the other axioms, not an axiom

Definition

Open ball, closed ball and sphere in a metric space

Definition

Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space

Lemma

The reverse triangle inequality |d(x,z) - d(y,z)| ≤ d(x,y) in any metric space

Lemma

|d(x,A) - d(y,A)| ≤ d(x,y), so the distance to a fixed nonempty set is 1-Lipschitz

Definition

The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement

Lemma

The absolute value makes ℝ a metric space: d(x,y) = |x-y| is a metric, its open balls are the intervals (x-r, x+r), and it is unbounded

Lemma

ℝⁿ as the set of functions n → ℝ, and d₁, d₂, d_∞ are metrics on it

Lemma

The supremum metric d_∞(f,g) = supₓ |f(x) - g(x)| is a metric on the bounded real-valued functions on a nonempty set

Theorem

Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed

Definition

Interior, closure, boundary, limit point, isolated point and dense subset of a metric space

Theorem

The closure of a nonempty A is {x : d(x,A) = 0}, equals A together with its limit points, and is the smallest closed superset

Definition

Convergence of a sequence in a metric space: xₖ → x iff d(xₖ, x) → 0 in ℝ

Lemma

A sequence in a metric space has at most one limit

Lemma

The balls B(x, 1/n), n ≥ 1, form a countable neighbourhood base at x, so every metric space is first countable

Theorem

A point lies in the closure of A iff some sequence in A converges to it, and a set is closed iff it is sequentially closed

Theorem

Distinct points of a metric space have disjoint balls around them

Definition

Continuity of a map between metric spaces, at a point and globally, in the ε-δ form

Theorem

Metric continuity characterisations, with countable choice for the sequential converse

Definition

Isometry, isometric embedding, and the subspace metric on a subset

Lemma

An isometric embedding is injective and carries the metric topology of the source onto the subspace topology of its image

Definition

Topologically, uniformly and Lipschitz equivalent metrics on a set

Theorem

Lipschitz equivalence implies uniform equivalence implies topological equivalence

Lemma

min(d,1) and d/(1+d) are metrics uniformly equivalent to d, so every metric space carries a bounded metric with the same topology

Remark

Which metric axiom list this library uses, the live naming fork between semimetric and pseudometric, and why extended metrics are not treated here

False statement

FALSE: in every metric space the closure of B(x,r) is the closed ball of radius r

False statement

FALSE: boundedness of a metric space is determined by its topology

Sources