Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26
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 discrete metric induces the discrete topology, in which every subset is clopen

Example

Let XX be any set and define δ:X×XR\delta : X \times X \to \mathbb{R} by

δ(x,y):={0if x=y,1if xy.\delta(x,y) := \begin{cases} 0 & \text{if } x = y, \\ 1 & \text{if } x \ne y. \end{cases}

Then:

  1. δ\delta is a metric on XX (Metric space: d(x,y)=0d(x,y) = 0 iff x=yx = y, symmetry, and the triangle inequality; pseudometric and ultrametric), the discrete metric.
  2. For xXx \in X and a real r>0r > 0: B(x,r)={{x}0<r1Xr>1,Bˉ(x,r)={{x}0<r<1Xr1,S(x,1)=X{x}.B(x,r) = \begin{cases} \{x\} & 0 < r \le 1 \\ X & r > 1 \end{cases}, \qquad \bar B(x,r) = \begin{cases} \{x\} & 0 < r < 1 \\ X & r \ge 1 \end{cases}, \qquad S(x,1) = X \setminus \{x\}.
  3. Every subset of XX is open, hence every subset is closed, hence every subset is clopen (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). The metric topology of δ\delta is the discrete topology, the collection of all subsets of XX.

The example is the standard source of counterexamples about balls: here the closed ball of radius 11 is the whole space while the closure of the open ball of radius 11 is a single point, and the sphere of radius 11 is everything except the centre while the boundary of the ball is empty.

Facts & Assumptions

Given: A set XX, the function δ\delta above, points x,y,zXx, y, z \in X, a real r>0r > 0, and a subset UXU \subseteq X.

[L2]

Balls: B(x,r)={y:δ(x,y)<r}B(x,r) = \{y : \delta(x,y) < r\}, Bˉ(x,r)={y:δ(x,y)r}\bar B(x,r) = \{y : \delta(x,y) \le r\} and S(x,r)={y:δ(x,y)=r}S(x,r) = \{y : \delta(x,y) = r\} (Open ball, closed ball and sphere in a metric space).

[L3]

Open and closed: UU is open when every point of it has a ball around it inside it; FF is closed when XFX \setminus F is open (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).

[L5]

Order: 0<10 < 1, so 010 \ne 1; a sum of a positive and a nonnegative real is positive, and inequalities may be compared by trichotomy and transitivity (The multiplicative identity is positive, Order is preserved by adding a constant and by adding inequalities, Ordered field, Complete ordered field (least-upper-bound property)).

Verification

technique · direct
1.1

Separation and symmetry: δ(x,y)=0\delta(x,y) = 0 holds exactly when x=yx = y, since the other value 11 is different from 00; and the defining clauses are unchanged when xx and yy are exchanged, since "x=yx = y" is.

L1L5
1.2

Triangle inequality: if x=zx = z then δ(x,z)=0\delta(x,z) = 0 and the right side is a sum of two values in {0,1}\{0,1\}, hence at least 00; and if xzx \ne z then yy cannot equal both xx and zz, so at least one of δ(x,y),δ(y,z)\delta(x,y), \delta(y,z) equals 11 while the other is 00 or 11, whence δ(x,y)+δ(y,z)1=δ(x,z)\delta(x,y) + \delta(y,z) \ge 1 = \delta(x,z).

L1L5
1.3

Balls: δ(x,x)=0<r\delta(x,x) = 0 < r always, so xB(x,r)x \in B(x,r); and for yxy \ne x one has δ(x,y)=1\delta(x,y) = 1, so yB(x,r)y \in B(x,r) exactly when 1<r1 < r, yBˉ(x,r)y \in \bar B(x,r) exactly when 1r1 \le r, and yS(x,1)y \in S(x,1) always. This is claim 2.

L2L5
2.1

Every subset is open: for UXU \subseteq X and xUx \in U the ball B(x,1)B(x,1) is {x}\{x\} by the computation of step 1.3, and {x}U\{x\} \subseteq U.

L2L3L5
2.2

Claim 1 holds: δ\delta satisfies (M1) and (M2) by step 1.1 and (M3) by step 1.2, so it is a metric on XX.

step 1.1step 1.2L1
3.1

Claim 3 holds: every subset is open by step 2.1, so for any FXF \subseteq X the complement XFX \setminus F is open and FF is closed; thus every subset is clopen and the metric topology is the full power set of XX. In particular each singleton {x}\{x\} is closed, in agreement with the closed-ball computation Bˉ(x,r)={x}\bar B(x,r) = \{x\} for 0<r<10 < r < 1 and the fact that closed balls are closed.

step 1.3step 2.1L3L4
4.1

Claims 1, 2 and 3 hold by steps 2.2, 1.3 and 3.1.

step 1.3step 2.2step 3.1

Remarks

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 24 results over 10 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources