Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27
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:ARf : A \to \mathbb{R} is continuous on AA if and only if the preimage of every open subset of R\mathbb{R} is the intersection with AA of an open subset of R\mathbb{R}, and dually for closed sets

Statement

Let ARA \subseteq \mathbb{R} and f:ARf : A \to \mathbb{R}. Call a set SAS \subseteq A relatively open in AA when S=UAS = U \cap A for some open URU \subseteq \mathbb{R}, and relatively closed in AA when S=GAS = G \cap A for some closed GRG \subseteq \mathbb{R} (Open subset of R\mathbb{R} (every point has a neighbourhood inside it), closed subset (complement open), and clopen). For VRV \subseteq \mathbb{R} write f1(V):={xA:f(x)V}f^{-1}(V) := \{\, x \in A : f(x) \in V \,\}. Then the following are equivalent.

  1. ff is continuous on AA (Continuity of f:ARf : A \to \mathbb{R} at a point of AA and on AA: the ε\varepsilon-δ\delta condition, its agreement with limxcf(x)=f(c)\lim_{x \to c} f(x) = f(c) at a limit point, and continuity at an isolated point).
  2. f1(V)f^{-1}(V) is relatively open in AA for every open VRV \subseteq \mathbb{R}.
  3. f1(F)f^{-1}(F) is relatively closed in AA for every closed FRF \subseteq \mathbb{R}.

"Relatively open" is defined here inline, and on purpose. At this point in the reading order this library has no subspace-topology item for R\mathbb{R}, and the metric one (Isometry, isometric embedding, and the subspace metric on a subset) may not be reached before Dictionary: for ARA \subseteq \mathbb{R} with the metric d(x,y)=xyd(x,y) = |x-y|, continuity and uniform continuity of f:ARf : A \to \mathbb{R} agree with the metric-space notions, the Lipschitz and Hölder conditions are the metric ones instantiated, and a subset of R\mathbb{R} is compact in the open-cover sense of R\mathbb{R} exactly when it is a compact metric subspace has said that the two vocabularies agree, which is later on this page. The phrase above is therefore an abbreviation for the displayed condition and nothing more.

The preimage is taken inside AA. f1(V)f^{-1}(V) is a subset of AA, never of R\mathbb{R}, so claim 2 does not say that preimages of open sets are open. They are open only when AA is itself open: then UAU \cap A is an intersection of two open sets, hence open (Arbitrary unions and finite intersections of open subsets of R\mathbb{R} are open, and dually for closed sets). For A=[0,1]A = [0,1] and ff the identity, f1((1,1/2))=[0,1/2)f^{-1}\bigl((-1,1/2)\bigr) = [0,1/2) is not open, and it is the trace on AA of the open set (1,1/2)(-1,1/2).

No choice principle is used. The open set witnessing claim 2 is not selected point by point; it is constructed as a single union over a family cut out by a property, which is the device the proof below makes explicit.

Facts & Assumptions

Given: A set ARA \subseteq \mathbb{R} and a function f:ARf : A \to \mathbb{R}; for VRV \subseteq \mathbb{R}, f1(V)={xA:f(x)V}f^{-1}(V) = \{\, x \in A : f(x) \in V \,\}.

[L1]

Continuity of ff at cAc \in A: for every real ε>0\varepsilon > 0 there is a real δ>0\delta > 0 with f(x)f(c)<ε|f(x) - f(c)| < \varepsilon for every xAx \in A satisfying xc<δ|x - c| < \delta; equivalently f(ANδ(c))Nε(f(c))f\bigl(A \cap N_{\delta}(c)\bigr) \subseteq N_{\varepsilon}(f(c)) (Continuity of f:ARf : A \to \mathbb{R} at a point of AA and on AA: the ε\varepsilon-δ\delta condition, its agreement with limxcf(x)=f(c)\lim_{x \to c} f(x) = f(c) at a limit point, and continuity at an isolated point, The ε\varepsilon-neighbourhood and the punctured ε\varepsilon-neighbourhood of a point of R\mathbb{R}).

[L2]

Open sets of R\mathbb{R}: UU is open when every xUx \in U has some Nε(x)UN_{\varepsilon}(x) \subseteq U; every neighbourhood Nε(x)N_{\varepsilon}(x) is itself open; a set is closed exactly when its complement is open (Open subset of R\mathbb{R} (every point has a neighbourhood inside it), closed subset (complement open), and clopen, The ε\varepsilon-neighbourhood and the punctured ε\varepsilon-neighbourhood of a point of R\mathbb{R}).

[L4]

Set algebra: for VRV \subseteq \mathbb{R} one has f1(RV)=Af1(V)f^{-1}(\mathbb{R} \setminus V) = A \setminus f^{-1}(V); and for URU \subseteq \mathbb{R}, A(UA)=(RU)AA \setminus (U \cap A) = (\mathbb{R} \setminus U) \cap A.

Proof

technique · direct
1.1

From 1 to 2: the canonical witness. Assume ff is continuous on AA and let VRV \subseteq \mathbb{R} be open. Define U  :=  {Nδ(x) : xf1(V), δR, δ>0, f(ANδ(x))V}.U \;:=\; \bigcup \bigl\{\, N_{\delta}(x) \ : \ x \in f^{-1}(V),\ \delta \in \mathbb{R},\ \delta > 0,\ f\bigl(A \cap N_{\delta}(x)\bigr) \subseteq V \,\bigr\}. The family being united is cut out by a property of the pair (x,δ)(x,\delta), so it is a set and nothing is selected from it. Each of its members is open by [L2], so UU is open by [L3].

L2L3
1.2

f1(V)UAf^{-1}(V) \subseteq U \cap A. Let xf1(V)x \in f^{-1}(V), so xAx \in A and f(x)Vf(x) \in V. Since VV is open, [L2] gives a real ε>0\varepsilon > 0 with Nε(f(x))VN_{\varepsilon}(f(x)) \subseteq V, and continuity at xx gives, by [L1], a real δ>0\delta > 0 with f(ANδ(x))Nε(f(x))Vf\bigl(A \cap N_{\delta}(x)\bigr) \subseteq N_{\varepsilon}(f(x)) \subseteq V. So this pair (x,δ)(x,\delta) contributes Nδ(x)N_{\delta}(x) to the union, and xNδ(x)x \in N_{\delta}(x) by [L2]. Hence xUx \in U, and xAx \in A.

L1L2
1.3

From 2 to 1. Assume claim 2, let cAc \in A and let a real ε>0\varepsilon > 0 be given. The set V:=Nε(f(c))V := N_{\varepsilon}(f(c)) is open by [L2], so f1(V)=UAf^{-1}(V) = U \cap A for some open URU \subseteq \mathbb{R}. Since f(c)f(c)=0<ε|f(c) - f(c)| = 0 < \varepsilon we have cf1(V)c \in f^{-1}(V), hence cUc \in U, and [L2] gives a real δ>0\delta > 0 with Nδ(c)UN_{\delta}(c) \subseteq U. Every xAx \in A with xc<δ|x - c| < \delta then lies in UA=f1(V)U \cap A = f^{-1}(V), so f(x)Nε(f(c))f(x) \in N_{\varepsilon}(f(c)), that is f(x)f(c)<ε|f(x) - f(c)| < \varepsilon. As cc and ε\varepsilon were arbitrary, ff is continuous on AA.

L1L2
2.1

UAf1(V)U \cap A \subseteq f^{-1}(V). Let yUAy \in U \cap A. Then yNδ(x)y \in N_{\delta}(x) for some pair (x,δ)(x,\delta) occurring in the union, so yANδ(x)y \in A \cap N_{\delta}(x) and therefore f(y)Vf(y) \in V by the defining property of that pair. Hence yf1(V)y \in f^{-1}(V).

step 1.1
3.1

Claim 2 holds. By steps 1.2 and 2.1, f1(V)=UAf^{-1}(V) = U \cap A with UU open, so f1(V)f^{-1}(V) is relatively open in AA; and VV was an arbitrary open subset of R\mathbb{R}.

step 1.1step 1.2step 2.1
4.1

2 and 3 are equivalent. Let FRF \subseteq \mathbb{R} be closed and put V:=RFV := \mathbb{R} \setminus F, which is open by [L2]. If claim 2 holds then f1(V)=UAf^{-1}(V) = U \cap A with UU open, and by [L4] f1(F)=Af1(V)=A(UA)=(RU)A,f^{-1}(F) = A \setminus f^{-1}(V) = A \setminus (U \cap A) = (\mathbb{R} \setminus U) \cap A , with RU\mathbb{R} \setminus U closed by [L2]; so f1(F)f^{-1}(F) is relatively closed. The converse runs the same computation in the other direction, starting from an open VV, putting F:=RVF := \mathbb{R} \setminus V and using f1(V)=Af1(F)f^{-1}(V) = A \setminus f^{-1}(F).

step 3.1L2L4
5.1

Statements 1, 2 and 3 are therefore equivalent, and the passage from 1 to 2 selected nothing.

step 3.1step 1.3step 4.1

Remarks

Depends on

Used by

Dependency tree · next 3 levels

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