Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

Distinct points of a metric space have disjoint balls around them

Statement

Let (X,d) be a metric space (Metric space: d(x,y)=0 iff x=y, symmetry, and the triangle inequality; pseudometric and ultrametric) and let p,q∈X with p≠q. Put r:=d(p,q)/2. Then r>0 and

B(p,r)∩B(q,r)=∅.

Both sets are open (Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed) and contain p respectively q (Open ball, closed ball and sphere in a metric space), so every metric space is Hausdorff: distinct points are separated by disjoint open sets (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).

Facts & Assumptions

Given: A metric space (X,d) and points p,q∈X with p≠q; write c:=d(p,q).

[L2]

Halving. For a real c>0 put 2:=1+1 and c/2:=c⋅2−1. Then 2>0, so 2≠0 and 2−1>0 (The multiplicative identity is positive, Order is preserved by adding a constant and by adding inequalities, Inverses of positives are positive, and reciprocation reverses order, Ordered field); hence c/2>0 (Sign rules for products and monotonicity of multiplication); and c/2+c/2=c(2⋅2−1)=c (Field).

[L3]

Adding two strict inequalities: a<b and a′<b′ give a+a′<b+b′ (Order is preserved by adding a constant and by adding inequalities).

[L4]

Trichotomy of the order of R: a<a is impossible, and a≠0 together with a≥0 gives a>0 (Complete ordered field (least-upper-bound property), Ordered field).

[L5]

Membership in a ball: z∈B(u,t) means d(u,z)<t; balls are open and contain their centres (Open ball, closed ball and sphere in a metric space, Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed).

Proof

technique · direct
1.1

Since p≠q, axiom (M1) gives c=d(p,q)≠0, and c≥0, so c>0 by trichotomy; hence r:=c/2 is a positive real with r+r=c.

givenL1L2L4
2.1

Suppose some z∈X lay in both B(p,r) and B(q,r), that is d(p,z)<r and d(q,z)<r; then symmetry and the triangle inequality give c=d(p,q)≤d(p,z)+d(z,q)=d(p,z)+d(q,z)<r+r=c, so c<c, which trichotomy forbids.

step 1.1L1L3L4L5
3.1

No such z exists, so B(p,r)∩B(q,r)=∅; both sets are open and contain p respectively q, so distinct points of (X,d) are separated by disjoint open sets.

step 1.1step 2.1L5∎

Remarks

Depends on

Used by

Dependency tree · two levels

20 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