CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29

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.

Refuted: a pointwise bounded family of continuous functions is equicontinuous. The spikes are bounded by $1$ everywhere and are not equicontinuous at $0$

Statement refuted

Refuted claim: a pointwise bounded family of continuous maps between metric spaces is equicontinuous (Equicontinuity at a point, uniform equicontinuity, and pointwise boundedness of a family of maps between metric spaces).

The witness is the family of moving spikes on $I : = [0, 1]$ already built in FALSE: a pointwise convergent sequence of continuous functions converges uniformly on every compact set: with $a_{k} : = 1 / ι (k + 2)$ (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field),

$f_{k} (t) = \frac{t}{a_{k}} (0 \leq t \leq a_{k}), f_{k} (t) = 2 - \frac{t}{a_{k}} (a_{k} \leq t \leq 2 a_{k}), f_{k} (t) = 0 (2 a_{k} \leq t \leq 1) .$

Every $f_{k}$ is continuous and takes values in $[0, 1]$ , so $F : = {f_{k} : k \in N}$ is pointwise bounded; but $F$ is not equicontinuous at $0$ , because $f_{k}$ climbs from $0$ to $1$ over an interval of length $a_{k}$ , and $a_{k}$ can be made smaller than any prescribed $δ$ .

Facts & Assumptions

Given: $I = [0, 1]$ with the metric $d (s, t) = ∣ s - t ∣$ inherited from $R$ (The absolute value makes $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, Isometry, isometric embedding, and the subspace metric on a subset, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length), the target $R$ with the same metric, the reals $a_{k} = 1 / ι (k + 2)$ , the spikes $f_{k}$ displayed above and the family $F = {f_{k} : k \in N}$ .

[L1]

Each $f_{k}$ is a well-defined continuous function $I \to R$ , $f_{k} (0) = 0$ , $f_{k} (a_{k}) = 1$ , and $0 < a_{k} \leq 1 / 2$ , so $a_{k} \in I$ (FALSE: a pointwise convergent sequence of continuous functions converges uniformly on every compact set, Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous, The canonical natural $ι (n) = n \cdot 1_{F}$ of a field, Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not, Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric).

[L2]

$0 \leq f_{k} (t) \leq 1$ for every $t \in I$ and every $k$ : the three formulas take values $t / a_{k} \in [0, 1]$ , $2 - t / a_{k} \in [0, 1]$ and $0$ respectively on their pieces (Maximum and minimum of a set, Every nonempty finite set of reals has a maximum and a minimum, Absolute value in an ordered field).

[L3]

A family $F$ is pointwise bounded when for each $t$ the set ${f (t) : f \in F}$ lies in some ball of the target, and equicontinuous at $a$ when for every real $ε > 0$ there is a real $δ > 0$ with $∣ f (t) - f (a) ∣ < ε$ for every $f \in F$ and every $t$ with $∣ t - a ∣ < δ$ (Equicontinuity at a point, uniform equicontinuity, and pointwise boundedness of a family of maps between metric spaces, Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space, Open ball, closed ball and sphere in a metric space, Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form).

[L4]

For every real $η > 0$ there is a natural $m \geq 1$ with $1 / ι (m) < η$ ; $ι$ is strictly increasing with $ι (n) > 0$ for $n \geq 1$ ; and $0 < u \leq v$ gives $0 < 1 / v \leq 1 / u$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ , Canonical naturals are positive and strictly increasing, Inverses of positives are positive, and reciprocation reverses order, The canonical natural $ι (n) = n \cdot 1_{F}$ of a field).

Counterexample

technique · direct

1.1

For every $t \in I$ the set ${f_{k} (t) : k \in N}$ is contained in $[0, 1]$ and hence in the ball $B (0, 2)$ of $R$ , so $F$ is pointwise bounded.

L2L3

1.2

Every member of $F$ is continuous.

1.3

Take $ε : = 1 / 2$ and let $δ > 0$ be any real; by [L4] there is a natural $m \geq 1$ with $1 / ι (m) < δ$ , and setting $k : = m$ gives $a_{k} = 1 / ι (m + 2) \leq 1 / ι (m) < δ$ , since $m + 2 > m$ and $ι$ is increasing.

L4choose

2.1

For that $k$ the point $a_{k}$ lies in $I$ and satisfies $∣ a_{k} - 0 ∣ = a_{k} < δ$ , while $∣ f_{k} (a_{k}) - f_{k} (0) ∣ = ∣ 1 - 0 ∣ = 1$ , which is not below $ε = 1 / 2$ .

step 1.3L1

3.1

So no $δ > 0$ serves the whole family at $ε = 1 / 2$ and the point $0$ : the family $F$ is not equicontinuous at $0$ , hence not equicontinuous.

step 1.3step 2.1L3

4.1

By steps 1.1, 1.2 and 3.1 the family $F$ is a pointwise bounded family of continuous functions that is not equicontinuous, so the claim is false.

step 1.1step 1.2step 3.1∎

Remarks

The values stay in $[0, 1]$ and the slopes do not. $f_{k}$ is Lipschitz with constant $1 / a_{k} = ι (k + 2)$ and with no smaller one, so the family has no common Lipschitz constant. That is the contrast with the previous example on this page, where fixing the constant at $1$ is exactly what produced uniform equicontinuity.
The failure is at one point only, and that is enough. The family is equicontinuous at every $t > 0$ : for $0 < δ < t / 2$ and $k$ large the spike is identically $0$ on the interval around $t$ , and the finitely many remaining members are individually continuous. Equicontinuity is required at every point, so failure at $0$ refutes the claim.
Both hypotheses of an Ascoli-type theorem are therefore needed, and neither implies the other: this family is pointwise bounded and not equicontinuous, and the $1$ -Lipschitz maps of the previous example are equicontinuous and not pointwise bounded.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

73 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

Equicontinuity (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 7 (standard reference, not scraped)

Refuted: a pointwise bounded family of continuous functions is equicontinuous. The spikes are bounded by 11 everywhere and are not equicontinuous at 00