Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adapted
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.

f:A→R is continuous at c∈A if and only if ωf(c)=0

Statement

Let A⊆R, let f:A→R and let c∈A. Then

f is continuous at c⟺ωf(c)=0

(Continuity of f:A→R at a point of A and on A: the ε-δ condition, its agreement with lim⁡x→cf(x)=f(c) at a limit point, and continuity at an isolated point, The oscillation ωf(S)=sup⁡{ ∣f(x)−f(y)∣:x,y∈S } of f on a set and the oscillation ωf(c)=inf⁡δ>0ωf(A∩Nδ(c)) at a point, both taken in the extended reals).

Since ωf(c)≥0 always (The oscillation ωf(S)=sup⁡{ ∣f(x)−f(y)∣:x,y∈S } of f on a set and the oscillation ωf(c)=inf⁡δ>0ωf(A∩Nδ(c)) at a point, both taken in the extended reals), the equivalent form of the right-hand side is: for every real ε>0 there is a real δ>0 with ωf(A∩Nδ(c))<ε.

This is the tool that converts a pointwise condition into a set condition. Continuity at c is a statement about f near c with a quantifier over ε; ωf(c)=0 is the vanishing of a single extended real attached to the point. The change of form is what makes the discontinuity set accessible: the sets { x∈A:ωf(x)≥ε } are relatively closed in A (For every real ε>0 the set { x∈A:ωf(x)≥ε } is the intersection with A of a closed subset of R; in particular it is closed in R when A=R) and their union over ε=1,1/2,1/3,… is the discontinuity set (For f:A→R the set of points of A at which f is discontinuous is the intersection with A of an Fσ subset of R, and the set of points at which f is continuous is the intersection with A of a Gδ subset; for A=R the two sets are Fσ and Gδ outright).

Facts & Assumptions

Given: A⊆R, a function f:A→R, and a point c∈A.

[L1]

f is continuous at c exactly when for every real ε>0 there is a real δ>0 with ∣f(x)−f(c)∣<ε for every x∈A with ∣x−c∣<δ; equivalently for every x∈A∩Nδ(c) (Continuity of f:A→R at a point of A and on A: the ε-δ condition, its agreement with lim⁡x→cf(x)=f(c) at a limit point, and continuity at an isolated point, The ε-neighbourhood and the punctured ε-neighbourhood of a point of R).

[L2]

ωf(S)=sup⁡{∣f(x)−f(y)∣:x,y∈S} and ωf(c)=inf⁡{ωf(A∩Nδ(c)):δ>0}, both in R‾; 0≤ωf(c)≤ωf(A∩Nδ(c)) for every real δ>0, and c∈A∩Nδ(c) (The oscillation ωf(S)=sup⁡{ ∣f(x)−f(y)∣:x,y∈S } of f on a set and the oscillation ωf(c)=inf⁡δ>0ωf(A∩Nδ(c)) at a point, both taken in the extended reals, The extended real line R‾=R∪{−∞,+∞}, its order, and the arithmetic that is left undefined).

[L3]

In R‾ every subset has a least upper bound and a greatest lower bound; a supremum is at most an extended real u exactly when u bounds every member of the set, and an infimum is at least an extended real ℓ exactly when ℓ bounds every member from below (Every subset of R‾ has a least upper bound and a greatest lower bound in R‾, agreeing with the real supremum and infimum on nonempty sets bounded in R).

[L4]

∣u−w∣≤∣u−v∣+∣v−w∣ for reals u,v,w, by applying The triangle inequality to (u−v)+(v−w)=u−w; and ∣u∣≥0 by Basic properties of the absolute value.

Proof

technique · direct
1.1L1

Suppose f is continuous at c and let ε>0 be real. Take δ>0 with ∣f(x)−f(c)∣<ε/2 for every x∈A∩Nδ(c).

1.2L2L3

Conversely, suppose ωf(c)=0 and let ε>0 be real. Not every member of {ωf(A∩Nδ(c)):δ>0} can be ≥ε, for then ε would be a lower bound of that set and the infimum ωf(c)=0 would satisfy 0≥ε. So there is a real δ>0 with ωf(A∩Nδ(c))<ε.

2.1step 1.1L2L3L4

For x,y∈A∩Nδ(c) with δ as in step 1.1, ∣f(x)−f(y)∣≤∣f(x)−f(c)∣+∣f(c)−f(y)∣<ε/2+ε/2=ε; so ε is an upper bound of the set whose supremum is ωf(A∩Nδ(c)), and therefore ωf(A∩Nδ(c))≤ε.

2.2step 1.2L2L3

With δ as in step 1.2 and any x∈A∩Nδ(c): both x and c lie in A∩Nδ(c), so ∣f(x)−f(c)∣ is one of the values whose supremum is ωf(A∩Nδ(c)) and therefore ∣f(x)−f(c)∣≤ωf(A∩Nδ(c))<ε.

3.1step 2.1L2L3

Hence 0≤ωf(c)≤ε for every real ε>0. If ωf(c) were not 0 it would satisfy 0<ωf(c)≤1, hence be a positive real, and taking ε:=ωf(c)/2 would give ωf(c)≤ωf(c)/2, which is false for a positive real. So ωf(c)=0.

4.1step 3.1step 2.2L1∎

Since ε>0 was arbitrary in step 1.2, the continuity condition holds at c, and f is continuous at c. Together with step 3.1 this proves the equivalence.

Remarks

Depends on

Dependency tree · 2 levels

Sources