Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passverified 2026-08-10 (gpt-5.6-terra-codex-subscription)
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 vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions

Statement

Let mNm \in \mathbb{N} with m1m \ge 1, with vector-valued functions, their components fi=πiff_i = \pi_i \circ f, their limits and their continuity as in Vector-valued functions f:ARmf : A \to \mathbb{R}^m, their limits and continuity, with the dictionary to the metric notions.

  1. Continuity is componentwise. Let (X,dX)(X,d_X) be a metric space, AXA \subseteq X, f:ARmf : A \to \mathbb{R}^{m} and aAa \in A. Then ff is continuous at aa if and only if every component fi:ARf_i : A \to \mathbb{R} (i<m)(i<m) is continuous at aa.
  2. Limits are componentwise. Let ARA \subseteq \mathbb{R}, let cc be a limit point of AA (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}), let f:ARmf : A \to \mathbb{R}^{m} and let LRmL \in \mathbb{R}^{m}. Then limxcf(x)=L\lim_{x\to c} f(x) = L if and only if limxcfi(x)=Li\lim_{x\to c} f_i(x) = L_i for every i<mi<m (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA).
  3. Algebra. Let (X,dX)(X,d_X), AA, aa be as in clause 1, let f,g:ARmf, g : A \to \mathbb{R}^{m} be continuous at aa and let λR\lambda \in \mathbb{R}. Then f+gf + g and λf\lambda f (defined pointwise) are continuous at aa; the real-valued function xf(x),g(x)x \mapsto \langle f(x), g(x)\rangle is continuous at aa (The Euclidean inner product x,y=k<nxkyk\langle x,y\rangle = \sum_{k<n} x_k y_k on Rn\mathbb{R}^n); and for every norm NN on Rm\mathbb{R}^{m} the real-valued function xN(f(x))x \mapsto N(f(x)) is continuous at aa (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms).

Where m1m \ge 1 is spent. The "if" direction of clauses 1 and 2 divides ε\varepsilon by ι(m)\iota(m), which requires ι(m)0\iota(m) \ne 0; and clause 3's last part quotes a bound available only for m1m \ge 1. The "only if" directions hold for every mm but say nothing at m=0m = 0, there being no index i<0i < 0.

Facts & Assumptions

Given: A natural m1m \ge 1; a metric space (X,dX)(X,d_X), a subset AXA \subseteq X, a point aAa \in A and functions f,g:ARmf, g : A \to \mathbb{R}^{m}; a real λ\lambda; and a real ε>0\varepsilon > 0.

[L2]

The comparison y2y1=i<myi\lVert y\rVert_2 \le \lVert y\rVert_1 = \sum_{i<m}|y_i|, and N(y)Cy1Cι(m)y2N(y) \le C\lVert y\rVert_1 \le C\sqrt{\iota(m)}\lVert y\rVert_2 with C:=max{N(ei):i<m}0C := \max\{N(e_i) : i<m\} \ge 0, together with N(y)N(z)N(yz)|N(y)-N(z)| \le N(y-z), all for m1m \ge 1 (The finite and reverse triangle inequalities for a norm; and for n1n \ge 1 every norm NN on Rn\mathbb{R}^n satisfies N(x)Cx1N(x) \le C\lVert x\rVert_1 and is Lipschitz, hence continuous, for d2d_2 clauses 1, 2, 3, The pp-norms xp\lVert x\rVert_p for rational p1p \ge 1, and x\lVert x\rVert_\infty, The standard list e:nFne : n \to F^{n} with ei(i)=1Fe_i(i) = 1_F and ei(j)=0Fe_i(j) = 0_F for jij \ne i is an ordered basis of FnF^{n}; hence dimFFn=n\dim_F F^{n} = n, and F0F^{0} is the zero space with basis \varnothing and dimension 00).

[L5]

Laws of finite sums (Laws of finite sums and finite products, Finite sums and finite products, by recursion): additivity, scaling, monotonicity, i<mμ=ι(m)μ\sum_{i<m}\mu = \iota(m)\mu, a sum of nonnegative terms is nonnegative, and each single term is at most such a sum.

[L7]

A nonempty finite set of reals has a minimum (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set); and a family of nonempty sets indexed by a natural number has a choice function, this being a theorem of ZF (Every natural-number-indexed list of nonempty sets has a choice function on its family of values), which is what licenses picking one δi\delta_i for each i<mi<m.

[L8]

Absolute value (Basic properties of the absolute value): t0|t| \ge 0, st=st|st| = |s||t|, and s+ts+t|s+t| \le |s|+|t|.

Proof

technique · direct
1.1

For every yRmy \in \mathbb{R}^{m}: yiy2|y_i| \le \lVert y\rVert_2 for each i<mi<m, and y2i<myi\lVert y\rVert_2 \le \sum_{i<m}|y_i|.

L1L2
1.2

If ai<bia_i < b_i for every i<mi<m and m1m \ge 1, then i<mai<i<mbi\sum_{i<m}a_i < \sum_{i<m}b_i: the list ibiaii \mapsto b_i - a_i has positive terms, so its sum is at least its term at index 00, hence positive, and additivity gives the strict inequality.

L5L6
1.3

For each i<mi<m the set of positive reals δ\delta witnessing continuity of fif_i at aa for a given tolerance is nonempty whenever fif_i is continuous at aa, so a choice function on the family indexed by mm produces δ0,,δm1\delta_0,\dots,\delta_{m-1} simultaneously, with no choice principle used.

L7
1.4

For f+gf+g: given ε>0\varepsilon > 0, pick δ1,δ2>0\delta_1, \delta_2 > 0 for the tolerance ε/ι(2)\varepsilon/\iota(2) at ff and at gg and put δ:=min{δ1,δ2}\delta := \min\{\delta_1,\delta_2\}; then for dX(x,a)<δd_X(x,a) < \delta, (f+g)(x)(f+g)(a)2=(f(x)f(a))+(g(x)g(a))2f(x)f(a)2+g(x)g(a)2<ε\lVert (f+g)(x)-(f+g)(a)\rVert_2 = \lVert (f(x)-f(a)) + (g(x)-g(a))\rVert_2 \le \lVert f(x)-f(a)\rVert_2 + \lVert g(x)-g(a)\rVert_2 < \varepsilon.

L1L3L6L7
1.5

For λf\lambda f: if λ=0\lambda = 0 then λf\lambda f is constant and every δ\delta serves; otherwise λ>0|\lambda| > 0, and a δ\delta for the tolerance ε/λ\varepsilon/|\lambda| at ff gives λf(x)λf(a)2=λf(x)f(a)2<ε\lVert \lambda f(x) - \lambda f(a)\rVert_2 = |\lambda|\,\lVert f(x)-f(a)\rVert_2 < \varepsilon.

L1L3L6L8
1.6

For NfN \circ f: by [L2], N(f(x))N(f(a))N(f(x)f(a))Cι(m)f(x)f(a)2|N(f(x)) - N(f(a))| \le N\bigl(f(x)-f(a)\bigr) \le C\sqrt{\iota(m)}\,\lVert f(x)-f(a)\rVert_2; so a δ\delta for the tolerance ε/(Cι(m)+1)\varepsilon/(C\sqrt{\iota(m)}+1) at ff serves for NfN\circ f.

L1L2L6
1.7

For f,g\langle f,g\rangle: first take δ0>0\delta_0 > 0 with g(x)g(a)2<1\lVert g(x)-g(a)\rVert_2 < 1 for dX(x,a)<δ0d_X(x,a) < \delta_0, so that g(x)2g(x)g(a)2+g(a)2<B:=g(a)2+1\lVert g(x)\rVert_2 \le \lVert g(x)-g(a)\rVert_2 + \lVert g(a)\rVert_2 < B := \lVert g(a)\rVert_2 + 1 there.

L1L3
2.1

Suppose ff is continuous at aa and fix i<mi<m. Given ε>0\varepsilon > 0, take δ\delta from the definition; for xAx \in A with dX(x,a)<δd_X(x,a) < \delta, step 1.1 gives fi(x)fi(a)f(x)f(a)2<ε|f_i(x)-f_i(a)| \le \lVert f(x)-f(a)\rVert_2 < \varepsilon. So fif_i is continuous at aa.

step 1.1L1
2.2

Conversely suppose every fif_i is continuous at aa. Given ε>0\varepsilon > 0, the real ε/ι(m)\varepsilon/\iota(m) is positive; by step 1.3 choose δi>0\delta_i > 0 for each i<mi<m with fi(x)fi(a)<ε/ι(m)|f_i(x)-f_i(a)| < \varepsilon/\iota(m) whenever xAx \in A and dX(x,a)<δid_X(x,a) < \delta_i, and put δ:=min{δ0,,δm1}>0\delta := \min\{\delta_0,\dots,\delta_{m-1}\} > 0.

step 1.3L1L6L7
2.3

By bilinearity, f(x),g(x)f(a),g(a)=f(x)f(a),g(x)+f(a),g(x)g(a)\langle f(x),g(x)\rangle - \langle f(a),g(a)\rangle = \langle f(x)-f(a),\, g(x)\rangle + \langle f(a),\, g(x)-g(a)\rangle, so Cauchy-Schwarz and step 1.7 give f(x),g(x)f(a),g(a)Bf(x)f(a)2+f(a)2g(x)g(a)2\bigl|\langle f(x),g(x)\rangle - \langle f(a),g(a)\rangle\bigr| \le B\,\lVert f(x)-f(a)\rVert_2 + \lVert f(a)\rVert_2\,\lVert g(x)-g(a)\rVert_2 for every xAx \in A with dX(x,a)<δ0d_X(x,a) < \delta_0.

step 1.7L4L8
3.1

For xAx \in A with dX(x,a)<δd_X(x,a) < \delta: each fi(x)fi(a)<ε/ι(m)|f_i(x)-f_i(a)| < \varepsilon/\iota(m), so by steps 1.1 and 1.2, f(x)f(a)2i<mfi(x)fi(a)<i<mε/ι(m)=ε\lVert f(x)-f(a)\rVert_2 \le \sum_{i<m}|f_i(x)-f_i(a)| < \sum_{i<m}\varepsilon/\iota(m) = \varepsilon. Hence ff is continuous at aa, and clause 1 is proved.

step 1.1step 1.2step 2.2L5L6
3.2

Clause 2 is the same two estimates with f(a)f(a) replaced by LL, fi(a)f_i(a) by LiL_i, and the condition dX(x,a)<δd_X(x,a) < \delta by 0<xc<δ0 < |x-c| < \delta: step 1.1 gives fi(x)Lif(x)L2|f_i(x)-L_i| \le \lVert f(x)-L\rVert_2 for the forward direction, and steps 1.1, 1.2 give f(x)L2i<mfi(x)Li<ε\lVert f(x)-L\rVert_2 \le \sum_{i<m}|f_i(x)-L_i| < \varepsilon for the converse, with δ\delta the minimum of mm radii obtained as in step 2.2.

step 1.1step 1.2step 1.3L1L5L6L7
3.3

Put P:=B+f(a)2+1>0P := B + \lVert f(a)\rVert_2 + 1 > 0 and take δδ0\delta \le \delta_0 positive with both f(x)f(a)2<ε/P\lVert f(x)-f(a)\rVert_2 < \varepsilon/P and g(x)g(a)2<ε/P\lVert g(x)-g(a)\rVert_2 < \varepsilon/P for dX(x,a)<δd_X(x,a) < \delta; then step 2.3 bounds the difference by (B+f(a)2)ε/P<ε(B + \lVert f(a)\rVert_2)\varepsilon/P < \varepsilon, so f,g\langle f,g\rangle is continuous at aa.

step 1.7step 2.3L1L6L7
4.1

Steps 1.4, 1.5, 1.6 and 3.3 are clause 3, and with steps 3.1 and 3.2 all three clauses are proved.

step 3.1step 3.2step 1.4step 1.5step 1.6step 3.3

Remarks

Depends on

Used by

Dependency tree · next 3 levels

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