Alphabeta Math
PropositionStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-16
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.

The general real function-algebra definition agrees with the published compact-metric definition

Statement

Let (K,d) be a nonempty compact metric space, and give K its metric topology. For a subset A⊆C(K,R), the following are equivalent:

  1. A is a unital point-separating real function algebra in the compact-metric sense of A unital point-separating real subalgebra of C(K,R);
  2. A is a unital point-separating real function algebra on the compact Hausdorff topological space K in the sense of Unital, point-separating, and nowhere-vanishing real function algebras on a compact Hausdorff space.

Under this identification the two ambient sets denoted C(K,R) are equal and their pointwise algebra operations agree.

Facts & Assumptions

Given: A nonempty compact metric space (K,d) with its metric topology, and a subset A of its real-valued continuous functions.

[L1]

For nonempty compact metric K, a subset of C(K,R) is a unital real function algebra when it contains every constant function and is closed under pointwise addition, real scalar multiplication, and multiplication; it separates points when every distinct pair is distinguished by one member (A unital point-separating real subalgebra of C(K,R)).

[L2]

The metric-space notation C(K,R) consists of the continuous functions from (K,d) to R with its usual metric (The space C(K,R) of continuous real-valued functions on a nonempty compact metric space).

[L3]

For maps between metric spaces, epsilon-delta continuity at every point is equivalent to the inverse image of every open set being open (Metric continuity characterisations, with countable choice for the sequential converse).

[L5]

Every metric space is Hausdorff: distinct points are separated by disjoint open balls (Distinct points of a metric space have disjoint balls around them).

[L6]

A real function algebra on a compact Hausdorff space is a real vector subspace of C(K,R) closed under pointwise multiplication; unitality means that it contains every constant function, and point separation means that every distinct pair is distinguished by one member (Unital, point-separating, and nowhere-vanishing real function algebras on a compact Hausdorff space).

Proof

technique · direct
1.1L4L5

By [L4] and [L5], the metric topology makes K a compact Hausdorff topological space.

1.2L2L3

By [L2] and the equivalence (a)⇔(b) in [L3], a function K→R is continuous in the metric sense exactly when it is continuous for the metric topologies, so the two ambient sets C(K,R) are equal.

2.1step 1.1step 1.2L1L6∎

The pointwise addition, scalar multiplication, and multiplication in [L1] and [L6] are the same operations on the common ambient set from step 1.2, and the constant-function and point-separation clauses have the same quantifiers; hence condition 1 implies condition 2 and condition 2 implies condition 1.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

41 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