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

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-domain-codomain-range/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-domain-codomain-range-01 · production-20261019-adopted-96



## 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

S01 · definitionBefore

f:A\to B

After

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

Conditions: none

Rule: mko_dcr_def · Uses: G3, mko_dcr_def

Leaf basis: mko_dcr_def + image_preimage_def

By the MKO: the domain A is the set of all permitted inputs, the codomain B is the declared output set, and the range f[A] collects only the outputs that actually occur. These are three different things: A and B are part of the declaration, while f[A] has to be computed.



S02 · impliesBefore

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

After

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

Conditions: none

Rule: numeric_evaluation · Uses: G1

Leaf basis: numeric_evaluation + power_laws

Compute each of the four inputs of A: (−1)²+1=2, 0²+1=1, 1²+1=2, 2²+1=5. Each input substituted into the rule gives exactly one number.



S03 · impliesBefore

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

After

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

Conditions: none

Rule: function_def · Uses: G1, S02, function_def

Leaf basis: function_def + set_builder

A total function needs: every input of A has an output, each input has exactly one output, and every output lies in B. S02 gives one value for each of the four inputs, and 2, 1, 2, 5 all belong to B={0,1,2,3,4,5}. So f:A→B is a total function.



S04 · equivalentBefore

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

After

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

Conditions: none

Rule: set_extensionality · Uses: S01, S02, set_extensionality

Leaf basis: set_extensionality + image_preimage_def + eq_replace

By definition the range is the set of all f(x) with x∈A. Substituting the values of S02 gives {2,1,2,5}. A set is determined by its elements, so the repeated 2 counts once and order is irrelevant: f[A]={1,2,5}, with 3 elements.



S05 · theorem_applicationBefore

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

After

f[A]\subseteq B

Conditions: none

Rule: L_range_sub · Uses: S03, S04, L_range_sub

Leaf basis: L_range_sub + subset_def

By Lemma L_range_sub the range of a total function is always a subset of its codomain; here one can also see directly that 1, 2 and 5 are in B.



S06 · impliesBefore

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

After

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

Conditions: none

Rule: set_extensionality · Uses: G1, S04

Leaf basis: set_extensionality + set_operations_def

0 belongs to B but is none of 1, 2, 5, so 0∉f[A]. The two sets have different elements, so by extensionality f[A]≠B. Likewise 3 and 4 lie in B but not in the range: B∖f[A]={0,3,4}. This is the MKO's point that the range need not equal B.



S07 · impliesBefore

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

After

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

Conditions: none

Rule: function_def · Uses: S02, function_def

Leaf basis: function_def + numeric_evaluation

Non-example one: if the same rule is declared with codomain B′={0,1,2,3,4}, the input 2 has output 5∉B′, violating 'outputs lie in the codomain', so this declaration is not a total function A→B′. The codomain may not be enlarged or ignored after the fact to accommodate an output.



S08 · impliesBefore

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

After

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

Conditions: none

Rule: function_def · Uses: G1, function_def

Leaf basis: function_def

Non-example two: a table listing only the inputs −1, 0 and 1 is claimed to be a function on A. But 2∈A has no output, violating 'every input of A has an output'. The set {1,2} read off this table is not f[A]; it misses 5. As the MKO says, the range of a claimed total function may not be computed from a table with undefined inputs.



S09 · impliesBefore

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

After

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

Conditions: none

Rule: function_def · Uses: S02, S04, function_def

Leaf basis: function_def + injective_surjective_def

Declare the same rule with codomain C={1,2,5}: every output 1, 2, 5 lies in C, so f_C:A→C is a total function. By function_def, equal functions need the same domain and codomain, and B≠C, so f_C and f have different defining data, although both have range {1,2,5}. For f_C the range equals the codomain (it is surjective); for f it does not.



S10 · impliesBefore

x\in\mathbb{R}

After

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

Conditions: none

Rule: L_shift · Uses: G2, square_nonneg, L_shift

Leaf basis: square_nonneg + L_shift + subset_def + forall_intro

h has a unique real value x²+1 at every real x, so h:ℝ→ℝ is a total function. Take any x∈ℝ: by square_nonneg, x²≥0, and by Lemma L_shift with u=x², x²+1≥1. So every output lies in [1,∞), that is h[ℝ]⊆[1,∞).



S11 · impliesBefore

y\in[1,\infty)

After

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

Conditions: y-1\geq 0

Rule: sqrt_def · Uses: L_shift, sqrt_def, interval_def

Leaf basis: sqrt_def + L_shift + interval_def

Take any y∈[1,∞), that is y≥1. By L_shift with u=y−1, using (y−1)+1=y, we get y−1≥0. A nonnegative real has a principal square root, so t=√(y−1) is a real number with t²=y−1.



S12 · impliesBefore

t^2=y-1

After

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

Conditions: none

Rule: image_preimage_def · Uses: G2, S11, image_preimage_def

Leaf basis: image_preimage_def + exists_intro + forall_intro + eq_replace

h(t)=t²+1=(y−1)+1=y. Since t is real, y is the output of some input, so y∈h[ℝ] by the definition of the range. As y was an arbitrary element of [1,∞), [1,∞)⊆h[ℝ]. For example y=10 gives t=√9=3 and h(3)=10.



S13 · impliesBefore

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

After

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

Conditions: none

Rule: set_extensionality · Uses: S10, S12, set_extensionality

Leaf basis: set_extensionality

Both inclusions are proved (S10, S12), so by extensionality h[ℝ]=[1,∞).



S14 · impliesBefore

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

After

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

Conditions: none

Rule: set_extensionality · Uses: S13, interval_def

Leaf basis: set_extensionality + interval_def + order_basics

0 is real but 0<1, so 0∉[1,∞)=h[ℝ]; that is, x²+1=0 has no real solution. The codomain ℝ and the range [1,∞) have different elements, so they are not equal: the declared codomain ℝ is not the set of actual outputs.



S15 · impliesBefore

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

After

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

Conditions: none

Rule: and_intro_elim · Uses: S03, S04, S05, S06, S07, S08, S13, S14

Leaf basis: and_intro_elim

Goal (1) is completed by S03 to S06, goal (2) by S07 and S08, and goal (3) by S13 and S14.







## Substeps and lemmas

S05.1 · impliesBefore

y\in f[A]

After

y\in B

Conditions: none

Rule: subset_def · Uses: image_preimage_def, function_def, subset_def

Leaf basis: image_preimage_def + function_def + subset_def + exists_elim + forall_intro

Take any y∈f[A]. By the definition of the range there is x∈A with y=f(x) (name it with a fresh letter). Since f is a total function A→B, f(x)∈B, hence y∈B. As y was arbitrary, f[A]⊆B by the definition of subset. This sub-step proves Lemma L_range_sub.



S10.1 · equivalentBefore

u\geq 0

After

u+1\geq 1

Conditions: none

Rule: order_basics · Uses: order_basics

Leaf basis: order_basics + add_inverse + add_assoc + add_zero

⇒: add 1 to both sides (a strict inequality is kept when u>0, and u=0 gives 1=1). ⇐: add −1 to both sides, using (u+1)+(−1)=u and 1+(−1)=0. This sub-step proves Lemma L_shift.







## 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 rangeThe 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 rangeThe 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 dataf: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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-domain-codomain-range-01.json)