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.

Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function

Statement

Let ARA \subseteq \mathbb{R}, let f,g:ARf, g : A \to \mathbb{R}, let αR\alpha \in \mathbb{R} and let cAc \in A. Suppose ff and gg are continuous at cc (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). Then:

  1. f+gf + g, αf\alpha f and fgfg are continuous at cc;
  2. f|f|, the function xf(x)x \mapsto |f(x)|, is continuous at cc;
  3. max{f,g}\max\{f,g\} and min{f,g}\min\{f,g\}, defined pointwise by xmax{f(x),g(x)}x \mapsto \max\{f(x), g(x)\} and xmin{f(x),g(x)}x \mapsto \min\{f(x), g(x)\} (Maximum and minimum of a set), are continuous at cc;
  4. if g(c)0g(c) \ne 0 then, writing A0:={xA:g(x)0}A_0 := \{\, x \in A : g(x) \ne 0 \,\}, the point cc lies in A0A_0 and the quotient (f/g)A0:A0R(f/g)|_{A_0} : A_0 \to \mathbb{R}, xf(x)/g(x)x \mapsto f(x)/g(x), is continuous at cc as a function on A0A_0.

Moreover, with no hypothesis at all:

  1. every constant function ARA \to \mathbb{R} and the identity id:AR\mathrm{id} : A \to \mathbb{R}, xxx \mapsto x, are continuous on AA; hence so is xxnx \mapsto x^{n} for every nNn \in \mathbb{N} (Integer powers ama^m), and hence so is every polynomial function xa0+a1x++anxnx \mapsto a_0 + a_1 x + \dots + a_n x^{n} with real coefficients.

Consequently, if ff and gg are continuous on AA then so are f+gf+g, αf\alpha f, fgfg, f|f|, max{f,g}\max\{f,g\} and min{f,g}\min\{f,g\}, and (f/g)A0(f/g)|_{A_0} is continuous on A0A_0.

Claim 4 is stated on A0A_0 because f/gf/g is not defined where gg vanishes, and gg may well vanish at points of AA far from cc. The hypothesis is g(c)0g(c) \ne 0, not "gg nowhere zero"; what it buys is that cc itself lies in the smaller domain, which is what makes continuity there mean anything.

Nothing here is proved through a sequence. Claims 1 and 4 are read off from Sums, scalar multiples, products and quotients of function limits, the quotient under the hypothesis that the denominator limit is nonzero, which is itself proved from ε\varepsilon and δ\delta, and claims 2, 3 and 5 are proved directly below. So no choice principle is used anywhere in this item.

Facts & Assumptions

Given: A set ARA \subseteq \mathbb{R}, functions f,g:ARf, g : A \to \mathbb{R}, a real α\alpha, a point cAc \in A at which ff and gg are continuous, and, for claim 4, the hypothesis g(c)0g(c) \ne 0 together with A0:={xA:g(x)0}A_0 := \{\, x \in A : g(x) \ne 0 \,\}.

[L1]

Continuity at cc: for every real ε>0\varepsilon > 0 there is a real δ>0\delta > 0 such that every xAx \in A with xc<δ|x - c| < \delta satisfies f(x)f(c)<ε|f(x) - f(c)| < \varepsilon (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).

[L3]

Algebra of function limits at a limit point cc of AA: if the limits of ff and gg at cc exist with values LL and MM, then the limits of f+gf+g, αf\alpha f and fgfg at cc exist with values L+ML+M, αL\alpha L and LMLM; and if M0M \ne 0 then cc is a limit point of A0A_0, and the limit of (f/g)A0(f/g)|_{A_0} at cc exists and equals L/ML/M (Sums, scalar multiples, products and quotients of function limits, the quotient under the hypothesis that the denominator limit is nonzero).

[L4]

Sign preservation: if the limit of gg at a limit point cc of AA exists and is nonzero, then cc is a limit point of A0={xA:g(x)0}A_0 = \{\, x \in A : g(x) \ne 0 \,\} (If limxcf(x)=L0\lim_{x \to c} f(x) = L \ne 0 then f>L/2|f| > |L|/2 on a punctured neighbourhood of cc; in particular if L>0L > 0 then f>L/2>0f > L/2 > 0 there).

[L5]

Reverse triangle inequality: uvuv\bigl||u| - |v|\bigr| \le |u - v| (The reverse triangle inequality); and u0|u| \ge 0, u=0|u| = 0 exactly when u=0u = 0, uv=uv|uv| = |u||v| (Basic properties of the absolute value).

[L6]

Maximum and minimum of a two-element set of reals exist (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set), and for all reals u,vu, v one has max{u,v}=12(u+v+uv)\max\{u,v\} = \tfrac{1}{2}\bigl(u + v + |u-v|\bigr) and min{u,v}=12(u+vuv)\min\{u,v\} = \tfrac{1}{2}\bigl(u + v - |u-v|\bigr).

[L7]

Ordered-field arithmetic in R\mathbb{R}: trichotomy and totality of the order, the field identities, and 0<10 < 1 so that 202 \ne 0 and t/2t/2 is defined (Ordered field, Field).

[L8]

Integer powers: a0=1a^{0} = 1 and an+1=anaa^{n+1} = a^{n} \cdot a (Integer powers ama^m).

Proof

technique · direct
1.1

Justification of the identity in [L6]. Let u,vRu, v \in \mathbb{R}. By totality either uvu \ge v or vuv \ge u. If uvu \ge v then uv0u - v \ge 0, so uv=uv|u-v| = u-v and 12(u+v+uv)=12(2u)=u=max{u,v}\tfrac{1}{2}(u+v+|u-v|) = \tfrac{1}{2}(2u) = u = \max\{u,v\}, while 12(u+vuv)=v=min{u,v}\tfrac{1}{2}(u+v-|u-v|) = v = \min\{u,v\}. If vuv \ge u the same computation with the roles exchanged applies, since uv=vu|u-v| = v-u there.

L5L6L7
1.2

The isolated case. Suppose cc is an isolated point of AA, say Nη(c)A={c}N_{\eta}(c) \cap A = \{c\} with η>0\eta > 0 real. Then every function on AA is continuous at cc by [L2], which gives claims 1, 2 and 3 at once. For claim 4, assume g(c)0g(c) \ne 0; then cA0c \in A_0, and Nη(c)A0Nη(c)A={c}N_{\eta}(c) \cap A_0 \subseteq N_{\eta}(c) \cap A = \{c\} with cc in the left-hand side, so cc is an isolated point of A0A_0 and every function on A0A_0, in particular (f/g)A0(f/g)|_{A_0}, is continuous at cc.

L2
1.3

Claim 2, at any point of AA. Let a real ε>0\varepsilon > 0 be given and let δ>0\delta > 0 be as in [L1] for ff and this ε\varepsilon. For xAx \in A with xc<δ|x - c| < \delta the reverse triangle inequality gives f(x)f(c)f(x)f(c)<ε\bigl||f(x)| - |f(c)|\bigr| \le |f(x) - f(c)| < \varepsilon. So f|f| is continuous at cc, and no case distinction was needed.

L1L5
1.4

Claim 5, constants and the identity. If ff is constant then f(x)f(c)=0<ε|f(x) - f(c)| = 0 < \varepsilon for every xAx \in A and every real ε>0\varepsilon > 0, so any δ>0\delta > 0 serves. For the identity, given a real ε>0\varepsilon > 0 take δ:=ε\delta := \varepsilon: every xAx \in A with xc<δ|x - c| < \delta has id(x)id(c)=xc<ε|\mathrm{id}(x) - \mathrm{id}(c)| = |x - c| < \varepsilon. Both are continuous at every point of AA.

L1L5L7
1.5

The limit-point case, claim 1. Suppose cc is a limit point of AA. By [L2] the limits of ff and of gg at cc exist and equal f(c)f(c) and g(c)g(c). By [L3] the limits of f+gf+g, αf\alpha f and fgfg at cc exist and equal f(c)+g(c)f(c)+g(c), αf(c)\alpha f(c) and f(c)g(c)f(c)g(c), which are exactly the values of those three functions at cc; by [L2] again, each of them is continuous at cc.

L2L3
1.6

The limit-point case, claim 4. Suppose cc is a limit point of AA and g(c)0g(c) \ne 0. Then cA0c \in A_0, and by [L4] the point cc is a limit point of A0A_0. By [L3] the limit of (f/g)A0(f/g)|_{A_0} at cc exists and equals f(c)/g(c)f(c)/g(c), which is the value of (f/g)A0(f/g)|_{A_0} at cc; by [L2] applied on the domain A0A_0, that function is continuous at cc.

L2L3L4
2.1

Claims 1 and 4 in general. By [L2] the point cc is either isolated in AA or a limit point of AA; step 1.2 settles the first case and steps 1.5 and 1.6 the second. So claims 1 and 4 hold as stated.

step 1.2step 1.5step 1.6L2
3.1

Claim 3. By claim 1 the function fg=f+(1)gf - g = f + (-1)g is continuous at cc, by step 1.3 so is fg|f-g|, and by claim 1 again so are f+g+fgf + g + |f-g| and its scalar multiple by 1/21/2. By step 1.1 that scalar multiple is the function xmax{f(x),g(x)}x \mapsto \max\{f(x), g(x)\}, so the maximum is continuous at cc; the same argument with fg-|f-g| gives the minimum.

step 1.1step 1.3step 2.1L6L7
3.2

Claim 5, powers and polynomials. The map xx0x \mapsto x^{0} is the constant 11 and xx1x \mapsto x^{1} is the identity, both continuous on AA by step 1.4; and if xxnx \mapsto x^{n} is continuous on AA then so is xxn+1=xnxx \mapsto x^{n+1} = x^{n} \cdot x, being a product of two functions continuous on AA by step 2.1. By induction on nn, xxnx \mapsto x^{n} is continuous on AA for every nNn \in \mathbb{N}. A polynomial function a0+a1x++anxna_0 + a_1x + \dots + a_nx^{n} is obtained from these by finitely many scalar multiplications and additions, each of which preserves continuity by step 2.1.

step 1.4step 2.1L8
4.1

Claims 1 to 5 are proved, all of them at an arbitrary point cc of AA and therefore, applied at every point, on the whole of AA; and no sequence and no choice principle was used.

step 1.3step 2.1step 3.1step 3.2

Remarks

Depends on

Used by

…and 28 more results.

Dependency tree · next 3 levels

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