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.
Open ball, closed ball and sphere in a metric space
Definition
Let be a metric space (Metric space: iff , symmetry, and the triangle inequality; pseudometric and ultrametric), let and let with (Order on the reals). Define
is the open ball, the closed ball and the sphere of centre and radius . The radius is always a strictly positive real; a ball of radius or of negative radius is never written in this library.
Immediate consequences of the definitions. For every and :
- , because (axiom (M1) of Metric space: iff , symmetry, and the triangle inequality; pseudometric and ultrametric); in particular open and closed balls are nonempty.
- and , and is the disjoint union of and , by trichotomy of the order of (Complete ordered field (least-upper-bound property), Ordered field): each satisfies exactly one of , , .
- If then and , by transitivity of the order.
- Nonnegativity of the metric (Nonnegativity of a metric is a consequence of the other axioms, not an axiom) is what forces the radius convention, and it forces it for the open ball only: if then is empty, because for every . The other two sets behave differently at , and the convention excludes them for uniformity rather than for emptiness: , since together with gives and hence by (M1). For all three sets are empty.
A sphere may be empty, and so the three sets are not on a par. For the open and closed balls always contain , but nothing in the definition produces a point at distance exactly from . If a metric takes only the values and , as the discrete metric on the companion page does, then while is the whole space. So nonemptiness of a sphere is never available by convention: where it is used, it is proved.
The ambient space is part of the notation. depends on and not on and alone. When more than one space or more than one metric is in play we write , or , and likewise for and . This matters as soon as subspaces appear (Isometry, isometric embedding, and the subspace metric on a subset): a ball of a subspace is the trace on it of a ball of the ambient space, and the two are different sets.
Definition references
Remarks
- The names "open ball" and "closed ball" are justified, not merely suggestive. That is an open set and a closed set in the metric topology is proved in Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed; the words are used here only as names for the three sets displayed above.
- The closed ball is not in general the closure of the open ball, and the sphere is not in general the boundary of either. Both failures are recorded on this page as FALSE: in every metric space the closure of is the closed ball of radius and witnessed on the companion page. The safe reading of the three names is the displayed one and nothing more.