LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-21

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.

A uniformly bounded equicontinuous sequence of $R^{n}$ -valued curves on a nonempty compact interval has a uniformly convergent subsequence

Statement

Let $J$ be a nonempty compact interval and $n \geq 1$ . Say that a sequence of continuous maps $x_{m} : J \to R^{n}$ is uniformly bounded when one $M$ satisfies $∥ x_{m} (t) ∥_{2} \leq M$ for all $m, t$ , and equicontinuous when for every $ε > 0$ there is $δ > 0$ such that $∣ s - t ∣ < δ$ implies $∥ x_{m} (s) - x_{m} (t) ∥_{2} < ε$ for every $m$ . Every such sequence has a subsequence that converges uniformly to a continuous map $x : J \to R^{n}$ . The construction requires no choice principle.

A uniformly bounded equicontinuous sequence of $R^{n}$ -valued curves on a nonempty compact interval has a uniformly convergent subsequence.

Facts & Assumptions

Given: The uniformly bounded equicontinuous sequence in the Statement.

[L1]

The rationals are countably infinite: $Q \approx N$ ( $Q$ is countably infinite).

[L3]

Continuous $R^{n}$ -valued curves on a compact interval are complete in the supremum metric (Continuous $R^{n}$ -valued curves on a nonempty compact interval form a complete supremum-metric space).

[L4]

Every closed bounded interval in $R$ is compact (Heine-Borel by bisection: every closed bounded interval $[a, b]$ is compact).

[L5]

The rationals are dense in $R$ (Both $Q$ and $R ∖ Q$ are dense in $R$ , and every nonempty open subset of $R$ is uncountable).

[L6]

Every nonempty subset of $N$ has a least element (The well-ordering principle).

[L7]

Euclidean space $R^{n}$ is complete for $n \geq 1$ ( $R$ and $R^{n}$ for $n \geq 1$ with the Euclidean metric are complete, componentwise from the Cauchy criterion in $R$ ).

[L8]

A total self-map and an initial value determine a unique sequence of iterates (The recursion theorem).

[L9]

If $0 < r < 1$ , then $r^{k} \to 0$ (For $∣ r ∣ < 1$ the sequence $r^{k}$ is null, and for $∣ r ∣ > 1$ the sequence $∣ r ∣^{k}$ diverges to $+ \infty$ ).

Proof

technique · constructive

1.1

Fix a time $q \in J$ and a strictly increasing index map $s : N \to N$ . Enclose the bounded sequence $(x_{s (j)} (q))_{j}$ in the cube $[- M, M]^{n}$ . Repeatedly bisect the current cube into its finitely many coordinate subcubes, retain the lexicographically first subcube containing infinitely many remaining terms, and take the least unused index whose value lies in it. The retained cubes are nested and their diameters tend to zero by [L9]; the selected values are therefore Cauchy and converge in $R^{n}$ by [L7]. Least indices exist by [L6]. This defines a specific strictly increasing extractor $E_{q} (s)$ whose selected values converge at $q$ , without making a choice from an unspecified family.

givenL6L7L9construct

2.1

If $J = {a}$ , use $E_{a}$ from step 1.1. Otherwise [L1] and [L5] give an enumeration $(q_{j})$ of the dense set $J \cap Q$ . Apply [L8] to the total update $(j, s) \mapsto (j + 1, s \circ E_{q_{j}} (s))$ , starting with the identity index map, and write the nested maps as $s_{j}$ . The diagonal indices $d_{j} = s_{j} (j)$ are strictly increasing. For each fixed $k$ , every sufficiently late $d_{j}$ lies in the range of $s_{k + 1}$ , so $(x_{d_{j}} (q_{k}))_{j}$ is a subsequence of the convergent sequence selected at $q_{k}$ . Thus $(x_{d_{j}})_{j}$ converges at every enumerated dense time, and the singleton construction has the same conclusion at its sole point.

step 1.1L1L5L8construct

3.1

Given $ε > 0$ , equicontinuity, [L4], and [L5] give a finite net of the dense times from step 2.1 on which the diagonal subsequence is eventually $ε / 3$ -close; in the singleton case use its sole point. The triangle inequality then makes the subsequence uniformly Cauchy on all of $J$ .

step 2.1L4L5algebra

4.1

Applying [L3] to the uniformly Cauchy subsequence gives a continuous uniform limit, completing the construction.

step 3.1L3discharge-construct∎

Depends on

Used by

Peano local existence for a continuous first-order system Theorem

Dependency tree · two levels

81 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

Gerald Teschl, Ordinary Differential Equations and Dynamical Systems, Ch. 2 (standard reference, not scraped)
Jiri Lebl, Basic Analysis I, Section 6.3 (standard reference, not scraped)

A uniformly bounded equicontinuous sequence of RnRn-valued curves on a nonempty compact interval has a uniformly convergent subsequence