Domain, codomain and range: a finite table and the range of h(x)=x²+1

Goal and scope

(1) With A={−1,0,1,2}, B={0,1,2,3,4,5} and f(x)=x²+1: verify that f:A→B is a total function, find the range f[A], and show f[A]⊆B but f[A]≠B; (2) explain why data with an output outside the declared codomain, or with a missing input, is not a total function in the sense of this entry; (3) for h:ℝ→ℝ, h(x)=x²+1, prove that the range is [1,∞), which differs from the codomain ℝ.

Inside the MKO's scope: total functions with explicitly stated A and B (assumption a1). The real part uses only that squares are nonnegative and that principal square roots exist. It does not treat partial functions, inverse functions, set-theoretic foundations or general methods for finding ranges, and does not change the canonical MKO or its English edition.

Givens and symbols

• function_def
• image_preimage_def
• set_extensionality
• subset_def
• square_nonneg
• sqrt_def
• order_basics
• numeric_evaluation

• G1 — A={−1,0,1,2}, B={0,1,2,3,4,5}, and f(x)=x²+1 for x∈A; the declared function is f:A→B.
• G2 — h:ℝ→ℝ with h(x)=x²+1.
• G3 — The defining data of a function are its domain, codomain and rule (MKO assumption a1: A and B are stated explicitly).

• A,\ B — domain and codomain
• f[A] — the range {f(x) ∣ x∈A}
• h — the real function h(x)=x²+1
• [1,\infty) — {y∈ℝ ∣ y≥1}
• \sqrt{u} — the principal square root of u≥0

Rules and sources

• function_def · prerequisite — Function: f:A→B assigns to each a∈A exactly one f(a)∈B. Two functions are equal ⇔ they have the same domain and codomain and agree at every a.
• image_preimage_def · prerequisite — Image and preimage: f(S)={f(a) ∣ a∈S}; f⁻¹(T)={a∈A ∣ f(a)∈T}. The preimage notation does not presuppose that f has an inverse.
• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B).
• square_nonneg · prerequisite — Squares are nonnegative: for every real u, u²≥0, and u²=0 ⇔ u=0.
• sqrt_def · prerequisite — Principal square root: for a≥0, √a is the unique real b with b≥0 and b²=a. Negative numbers have no real square root.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• power_laws · prerequisite — Integer exponent laws (base nonzero, or exponents positive integers): a^m·a^n=a^{m+n}, (a^m)^n=a^{mn}, (ab)^n=a^n b^n, a^0=1.
• set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• exists_elim · prerequisite — ∃-elimination: from ∃x∈D, P(x) we may name some element a with P(a) by a fresh name; reasoning with a is allowed as long as the final conclusion does not mention a.
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• set_operations_def · prerequisite — Set operations: x∈A∪B ⇔ x∈A or x∈B; x∈A∩B ⇔ x∈A and x∈B; x∈A∖B ⇔ x∈A and x∉B; in a universe U, Aᶜ=U∖A.
• injective_surjective_def · prerequisite — Injective: f(a)=f(a′) ⇒ a=a′. Surjective: every b∈B has some a∈A with f(a)=b. Bijective: both; then there is a unique inverse f⁻¹ with f⁻¹∘f=id_A and f∘f⁻¹=id_B.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
• add_zero · prerequisite — Additive identity: u+0=u.
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_dcr_def · cited — For a total function f:A→B, A is the set of all permitted inputs and B is the declared output set. The range f[A]={f(x):x∈A} is a subset of B and need not equal B. · mko-domain-codomain-range
• interval_def · prerequisite — [1,∞)={y∈ℝ ∣ y≥1}.
• L_range_sub · lemma — For every total function f:A→B, f[A]⊆B.
• L_shift · lemma — For a real u: u≥0 ⇔ u+1≥1.

Main derivation

f:A\to B

\text{domain}\ A,\ \text{codomain}\ B,\ f[A]=\{f(x)\mid x\in A\}

f(x)=x^2+1,\ x\in A

f(-1)=2,\ f(0)=1,\ f(1)=2,\ f(2)=5

f(-1)=2,\ f(0)=1,\ f(1)=2,\ f(2)=5

f:A\to B\ \text{is a total function}

f[A]=\{f(-1),f(0),f(1),f(2)\}

f[A]=\{2,1,2,5\}=\{1,2,5\}

f[A]=\{1,2,5\}

f[A]\subseteq B

f[A]=\{1,2,5\},\ B=\{0,1,2,3,4,5\}

0\in B\setminus f[A],\ \text{so}\ f[A]\neq B;\ B\setminus f[A]=\{0,3,4\}

\text{rule}\ x^2+1\ \text{declared as}\ A\to B'=\{0,1,2,3,4\}

f(2)=5\notin B':\ \text{not a total function}\ A\to B'

\text{table}\ \{(-1,2),(0,1),(1,2)\}\ \text{claimed as a function on}\ A

2\in A\ \text{has no output: not total on}\ A

f_C:A\to C=\{1,2,5\},\ f_C(x)=x^2+1

f_C\neq f\ \text{as function data},\ f_C[A]=\{1,2,5\}=C

x\in\mathbb{R}

h(x)=x^2+1\geq 1,\ \text{so}\ h[\mathbb{R}]\subseteq[1,\infty)

y\in[1,\infty)

y-1\geq 0,\ \ t=\sqrt{y-1}\in\mathbb{R},\ \ t^2=y-1

t^2=y-1

h(t)=(y-1)+1=y,\ \text{so}\ y\in h[\mathbb{R}]

h[\mathbb{R}]\subseteq[1,\infty),\ [1,\infty)\subseteq h[\mathbb{R}]

h[\mathbb{R}]=[1,\infty)

h[\mathbb{R}]=[1,\infty)

0\in\mathbb{R}\setminus h[\mathbb{R}],\ \text{so}\ h[\mathbb{R}]\neq\mathbb{R}

S03\ \text{to}\ S08,\ S13,\ S14

f[A]=\{1,2,5\}\subsetneq B;\ \ h[\mathbb{R}]=[1,\infty)\neq\mathbb{R}

Substeps and lemmas

y\in f[A]

y\in B

u\geq 0

u+1\geq 1

Reverse audits

• S15 · sufficient_goal_reduction · S03, S04, S05, S06, S07, S08, S13, S14, and_intro_elim — Goal G: (1) to (3). Sufficient condition H: the listed steps hold; H⇒G by conjunction introduction. H is proved forwards from the definitions, lemmas and computation; G is never used as a premise.
• S14 · premise_audit · S13, interval_def, order_basics — One element in the codomain but not in the range suffices to show they differ.
• S13 · premise_audit · S10, S12, set_extensionality — Set equality needs both directions; S10 alone would show only that the range is contained in [1,∞).
• S12 · premise_audit · S11, image_preimage_def, exists_intro, forall_intro — Each y needs only one input; the input is not claimed to be unique (−t also gives y).
• S11 · premise_audit · L_shift, sqrt_def — Taking the square root needs y−1≥0; if y<1 then y−1<0 has no real square root, which matches y not being in the range.
• S10.1 · inverse_equivalence · order_basics, add_inverse — Adding 1 and adding −1 undo each other and are possible for every real, so the step holds both ways (N9).
• S10 · premise_audit · square_nonneg, L_shift, subset_def — This is the ⊆ direction; the ⊇ direction (every y≥1 is attained) needs S11 and S12.
• S09 · premise_audit · function_def, S04, injective_surjective_def — The conclusion depends on the codomain being part of a function's defining data; the codomain cannot be read off an output table (second paragraph of the MKO).
• S08 · premise_audit · function_def, G1 — A single input without an output suffices to refute totality.
• S07 · premise_audit · S02, function_def — One output outside the declared codomain is enough to refute it; N5 checks 5>4.
• S06 · premise_audit · S04, set_extensionality, set_operations_def — Inequality needs only one element of B outside f[A]; here it is 0.
• S05.1 · premise_audit · image_preimage_def, function_def, subset_def, exists_elim — Only the condition 'outputs must lie in the codomain' is used; if outputs outside B were allowed (as in S07), the conclusion would fail.
• S05 · premise_audit · L_range_sub, S03 — The lemma needs f to really be a total function A→B (S03). Only inclusion is claimed, not equality.
• S04 · inverse_equivalence · set_extensionality, image_preimage_def — Both sides have the same elements, so by extensionality they are the same set, in both directions.
• S03 · premise_audit · S02, function_def — All three conditions must be checked input by input; S07 and S08 are non-examples that each miss one condition.
• S02 · premise_audit · G1, numeric_evaluation — The four values can be recomputed independently (N1 to N4); every element of A is covered.
• S01 · premise_audit · G3, mko_dcr_def — This step only states the definitions and derives no new fact.

Error controls and negative controls

The codomain is not the range

The first mistake named by the MKO is taking the codomain to be the actual range. The codomain B of f has 6 elements, but the range is only {1,2,5}; the codomain of h is ℝ, but the range is [1,∞). The codomain declares where outputs must land; the range is computed from the actual outputs, and the two coincide only for a surjection.

Check totality before computing a range

The second mistake named by the MKO is computing the range of a claimed total function from a table with undefined inputs. A table missing the input 2 gives {1,2} and loses 5; an output 5 outside the declared {0,1,2,3,4} means the declaration is not a function at all. Check the three conditions input by input first (S03); only then does the range make sense.

Changing the codomain changes the function's defining data

f:A→B and f_C:A→{1,2,5} give the same value at every input and have the same range, but their codomains differ, so they have different defining data; the first is not surjective and the second is. The codomain cannot be read off an output table (second paragraph of the MKO).

• The range of f:A→B is B={0,1,2,3,4,5} → reject — f[A]={1,2,5}; 0, 3 and 4 are not outputs of any input.
• The range of h:ℝ→ℝ, h(x)=x²+1, is ℝ → reject — x²+1≥1, so 0 is not in the range; the range is [1,∞).
• The table listing only −1, 0, 1 is a total function on A with range {1,2} → reject — 2∈A has no output; the true f[A] also contains 5.
• The rule x²+1 can be declared as a total function A→{0,1,2,3,4} → reject — f(2)=5 is not in {0,1,2,3,4}.
• The range {2,1,2,5} has four elements → reject — Repeated outputs count once; f[A]={1,2,5} has 3 elements.

Result and limitations

f:A→B with A={−1,0,1,2}, B={0,1,2,3,4,5} and f(x)=x²+1 is a total function with range f[A]={1,2,5}⊆B, but 0, 3 and 4 are not in the range, so f[A]≠B. Data with output 5 outside {0,1,2,3,4}, or missing the input 2, is not a total function in this entry's sense. The range of h:ℝ→ℝ, h(x)=x²+1, is [1,∞), which is not the codomain ℝ.

• N6 is a finite check at the integers x from −20 to 20 and supports only those points; the general fact x²+1≥1 comes from the argument of S10.

Verification and source binding

11 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 8bda61e820ecd87d075b98c8407ebfb669c073e33b1825b598e48d1e4176933c
• original source SHA-256: 8bda61e820ecd87d075b98c8407ebfb669c073e33b1825b598e48d1e4176933c
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)