ExampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27

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 bounded real-valued functions on a set, with the supremum metric, form a complete metric space

Example

Let $S$ be a nonempty set, let $\mathcal{B}(S) := \{\, f : f \text{ is a bounded function } S \to \mathbb{R} \,\}$ , and let $d_\infty(f,g) := \sup\{\, |f(s)-g(s)| : s \in S \,\}$ be the supremum metric, which is a metric on $\mathcal{B}(S)$ (The supremum metric $d_\infty(f,g) = \sup_x |f(x) - g(x)|$ is a metric on the bounded real-valued functions on a nonempty set, Lower bound, bounded below, bounded set).

Then $(\mathcal{B}(S), d_\infty)$ is a complete metric space (Complete metric space: every Cauchy sequence converges in the space).

The limit is produced pointwise and then shown to be bounded and to be approached uniformly; that order is the content of the proof.

Facts & Assumptions

Given: A nonempty set $S$ ; the space $\mathcal{B}(S)$ with the supremum metric $d_\infty$ ; a Cauchy sequence $(f_k)$ in $(\mathcal{B}(S), d_\infty)$ ; a point $s \in S$ ; a real $\varepsilon > 0$ .

[A1]

Cauchyness of $(f_k)$ : for every real $\varepsilon > 0$ there is $K$ with $d_\infty(f_k,f_l) < \varepsilon$ for all $k,l \ge K$ (Cauchy sequence in a metric space, The rationals embed densely in the reals).

[L1]

$d_\infty$ is a metric on $\mathcal{B}(S)$ , and $d_\infty(f,g)$ is the least upper bound of $\{|f(s)-g(s)| : s \in S\}$ , so it dominates each of those numbers and is dominated by every upper bound of them (The supremum metric $d_\infty(f,g) = \sup_x |f(x) - g(x)|$ is a metric on the bounded real-valued functions on a nonempty set, Complete ordered field (least-upper-bound property), Metric space: $d(x,y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric).

[L2]

A function $h : S \to \mathbb{R}$ is bounded when its range is a bounded subset of $\mathbb{R}$ , that is when there is a real $M \ge 0$ with $|h(s)| \le M$ for every $s$ ; the passage from a pair of bounds to a single $M$ is the maximum of two absolute values (Lower bound, bounded below, bounded set, Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set, Basic properties of the absolute value).

[L3]

Every Cauchy sequence of reals converges, and the limit of a real sequence is unique, which licenses $\lim_k a_k$ for a sequence already known to converge (The Cauchy criterion from the least-upper-bound property: in a complete ordered field every Cauchy sequence converges, A sequence has at most one limit, Limits and Cauchy sequences of reals).

[L4]

Limits of reals preserve non-strict inequalities holding eventually, and behave additively (Limits preserve non-strict inequalities, Algebra of limits: sums, scalar multiples, products and quotients).

[L5]

$\big||a| - |b|\big| \le |a-b|$ for reals, the reverse triangle inequality of the usual metric of $\mathbb{R}$ with third point $0$ ; hence $a_k \to a$ gives $|a_k| \to |a|$ (The reverse triangle inequality $|d(x,z) - d(y,z)| \le d(x,y)$ in any metric space, Basic properties of the absolute value, The absolute value makes $\mathbb{R}$ 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).

[L6]

Convergence in a metric space may be tested with real $\varepsilon > 0$ (Convergence of a sequence in a metric space: $x_k \to x$ iff $d(x_k, x) \to 0$ in $\mathbb{R}$ , The rationals embed densely in the reals).

Verification

technique · direct

1.1

For every $s \in S$ and all $k,l$ the number $|f_k(s) - f_l(s)|$ belongs to the set whose supremum is $d_\infty(f_k,f_l)$ , so $|f_k(s) - f_l(s)| \le d_\infty(f_k,f_l)$ .

1.2

Apply [A1] with $\varepsilon = 1$ to get $K_1$ with $d_\infty(f_k,f_l) < 1$ for all $k,l \ge K_1$ , and let $M \ge 0$ satisfy $|f_{K_1}(s)| \le M$ for every $s$ , which exists because $f_{K_1}$ is bounded.

A1L2

2.1

Hence for each fixed $s$ the real sequence $\big(f_k(s)\big)_k$ is Cauchy, by [A1] and step 1.1; so it converges, and its limit is unique, so $f(s) := \lim_k f_k(s)$ defines a function $f : S \to \mathbb{R}$ . No choice is used, each value being a unique limit.

step 1.1A1L3

2.2

Let $\varepsilon > 0$ be real and take $K$ from [A1] for $\varepsilon/2$ , so $d_\infty(f_k,f_l) < \varepsilon/2$ for all $k,l \ge K$ . For a fixed $s$ and a fixed $k \ge K$ we get $|f_k(s) - f_l(s)| \le d_\infty(f_k,f_l) < \varepsilon/2$ for every $l \ge K$ .

step 1.1A1

3.1

For every $s$ and every $l \ge K_1$ : $|f_l(s)| \le |f_{K_1}(s)| + |f_l(s) - f_{K_1}(s)| \le M + 1$ by step 1.1; letting $l$ grow and using $|f_l(s)| \to |f(s)|$ gives $|f(s)| \le M + 1$ . So $f$ is bounded and $f \in \mathcal{B}(S)$ .

step 1.1step 2.1step 1.2L2L4L5

3.2

step 2.1step 2.2L4L5

4.1

So $\varepsilon/2$ is an upper bound of $\{\,|f_k(s) - f(s)| : s \in S\,\}$ for every $k \ge K$ , whence $d_\infty(f_k, f) \le \varepsilon/2 < \varepsilon$ ; note that $d_\infty(f_k,f)$ is defined, both functions being bounded.

step 3.1step 3.2L1

5.1

Since $\varepsilon > 0$ was an arbitrary real, $f_k \to f$ in $(\mathcal{B}(S), d_\infty)$ with $f \in \mathcal{B}(S)$ ; every Cauchy sequence therefore converges, and $(\mathcal{B}(S), d_\infty)$ is complete.

step 3.1step 4.1L6∎

Remarks

The two limits are taken in different orders, and that is the point. Step 2.1 fixes $s$ and lets $k$ grow, producing a candidate limit function; steps 2.2 to 4.1 fix $k$ and let the other index grow inside an estimate that is uniform in $s$ . It is the uniformity of the bound $\varepsilon/2$ in $s$ , and nothing else, that converts pointwise convergence into convergence in $d_\infty$ .
Boundedness of the limit is a separate step and is genuinely needed. The metric $d_\infty(f_k,f)$ is only defined once $f$ is known to be bounded (The supremum metric $d_\infty(f,g) = \sup_x |f(x) - g(x)|$ is a metric on the bounded real-valued functions on a nonempty set), so step 3.1 has to come before step 4.1. The extended real line is introduced later, but it is not used as a metric codomain or as a placeholder here; $d_\infty(f_k,f)$ is real-valued only after boundedness of $f$ is proved.
Nothing is assumed about $S$ beyond nonemptiness, which is what The supremum metric $d_\infty(f,g) = \sup_x |f(x) - g(x)|$ is a metric on the bounded real-valued functions on a nonempty set needs so that the supremum is taken over a nonempty set. In particular $S$ carries no topology and no metric here; the functions are arbitrary bounded functions, not continuous ones.
Where the least-upper-bound property is spent. Twice: inside The Cauchy criterion from the least-upper-bound property: in a complete ordered field every Cauchy sequence converges at step 2.1, and in the very definition of $d_\infty$ (The supremum metric $d_\infty(f,g) = \sup_x |f(x) - g(x)|$ is a metric on the bounded real-valued functions on a nonempty set). Completeness of $\mathbb{R}$ is the whole engine of this example.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 105 results over 31 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

Uniform norm (Wikipedia) (standard reference, not scraped)
Complete metric space (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 7 (standard reference, not scraped)