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

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 function on a subset of $\mathbb{R}^m$ is continuous at $x$ iff its oscillation there is $0$ , and every oscillation superlevel set is closed

Statement

For $f:A\to\mathbb R$ , $f$ is continuous at $c\in A$ if and only if $\omega_f(c)=0$ . If $f$ is bounded, then for every $\varepsilon>0$ , the relative superlevel set $\{c\in A:\omega_f(c)\ge\varepsilon\}$ is closed in $A$ .

Facts & Assumptions

Given: $f,A,c$ .

[L1]

Metric continuity and balls are Continuity of a map between metric spaces, at a point and globally, in the $\varepsilon$ - $\delta$ form and Open ball, closed ball and sphere in a metric space.

[L2]

Oscillation is Oscillation of a real function on subsets of $\mathbb{R}^m$ and at a point.

Proof

technique · direct

1.1

If $f$ is continuous at $c$ , choose a ball on which $|f(x)-f(c)|<\varepsilon/3$ ; pairwise differences are then below $2\varepsilon/3$ , so the ball oscillation is at most $2\varepsilon/3<\varepsilon$ and $\omega_f(c)=0$ .

L1L2

1.2

If $\omega_f(c)=0$ , choose $r$ with ball oscillation below $\varepsilon$ . Holding one point at $c$ gives $|f(x)-f(c)|<\varepsilon$ , proving continuity.

L1L2

1.3

If $\omega_f(c)<\varepsilon$ , choose $r$ with $\omega_f(A\cap B(c,r))<\varepsilon$ . Every $d\in A\cap B(c,r/2)$ has a sufficiently small ball contained in $B(c,r)$ , so $\omega_f(d)<\varepsilon$ . Thus the sublevel set is relatively open.

L1L2given

2.1

Steps 1.1 and 1.2 give the equivalence; step 1.3 makes the complementary superlevel set closed.

step 1.1step 1.2step 1.3given∎

Depends on

Used by

Lebesgue's criterion in ℝᵐ: a bounded function on a closed nondegenerate rectangle is Riemann integrable iff its discontinuity set is null Theorem

Dependency tree · next 3 levels

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

J. Lebl, Basic Analysis, Riemann Integral in Several Variables (standard reference, not scraped)
J. Lebl, Basic Analysis, The Riemann-Lebesgue Criterion (standard reference, not scraped)

A function on a subset of Rm\mathbb{R}^mRm is continuous at xxx iff its oscillation there is 000, and every oscillation superlevel set is closed