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

Semicontinuity on Rn is characterized by strict open level sets and weak closed level sets

Statement

Let n1, let ARn, and let f:AR.

  • Upper semicontinuity is equivalent to relative openness of every strict sublevel set {f<α} and to relative closedness of every weak superlevel set {fα}.
  • Lower semicontinuity is equivalent to relative openness of every strict superlevel set and to relative closedness of every weak sublevel set.

Relative openness and closedness refer to the subspace topology on A (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace, The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement).

Facts & Assumptions

Given: The subset and function in the Statement, with Euclidean balls as in Open ball, closed ball and sphere in a metric space.

[F1]

The function f is upper semicontinuous at a when for every ε>0 there is δ>0 such that f(x)<f(a)+ε for every xAB2(a,δ); the lower clause is its one-sided dual (Upper and lower semicontinuity on subsets of Rn).

Proof

technique · direct
1.1

For the upper-semicontinuous forward direction, if f(c)<α, apply [F1] with ε=αf(c) to obtain a relative ball inside {f<α}. Conversely, if all strict sublevels are relatively open, the sublevel {f<f(c)+ε} supplies the ball required by [F1].

F1algebra
2.1

Taking complements in A converts the relatively open strict sublevels of step 1.1 into relatively closed weak superlevels and conversely. Thus both upper-semicontinuity characterisations hold in both directions.

step 1.1F1
3.1

Apply steps 1.1 and 2.1 to f. The lower clause for f is the upper clause for f, strict superlevels of f are strict sublevels of f, and weak sublevels of f are weak superlevels of f. This gives both lower-semicontinuity equivalences in both directions.

step 1.1step 2.1F1algebra

Depends on

Used by

Dependency tree · two levels

15 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