LemmaStatement: AI-adaptedProof: AI-adaptedprecheck 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 $R^{m}$ is continuous at $x$ iff its oscillation there is $0$ , and every oscillation superlevel set is closed

Statement

For $f : A \to R$ , $f$ is continuous at $c \in A$ if and only if $ω_{f} (c) = 0$ . If $f$ is bounded, then for every $ε > 0$ , the relative superlevel set ${c \in A : ω_{f} (c) \geq ε}$ 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 $ε$ - $δ$ form and Open ball, closed ball and sphere in a metric space.

[L2]

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

Proof

technique · direct

1.1L1L2

If $f$ is continuous at $c$ , choose a ball on which $∣ f (x) - f (c) ∣ < ε / 3$ ; pairwise differences are then below $2 ε / 3$ , so the ball oscillation is at most $2 ε / 3 < ε$ and $ω_{f} (c) = 0$ .

1.2L1L2

If $ω_{f} (c) = 0$ , choose $r$ with ball oscillation below $ε$ . Holding one point at $c$ gives $∣ f (x) - f (c) ∣ < ε$ , proving continuity.

1.3L1L2given

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

2.1step 1.1step 1.2step 1.3given∎

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

A function on a subset of $R^{m}$ is continuous at $x$ iff its oscillation there is $0$ , and every oscillation superlevel set is closed

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

A function on a subset of RmRm is continuous at xx iff its oscillation there is 00, and every oscillation superlevel set is closed

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

A function on a subset of $R^{m}$ is continuous at $x$ iff its oscillation there is $0$ , and every oscillation superlevel set is closed