Function mapping: deciding whether a rule is a function, and separating codomain, range and graph

Goal and scope

Let X={−2,−1,0,1,2}, Y={0,1,2,3,4,5} and f:X→Y, f(x)=x². Prove that f is a function; compute the range f(X)={0,1,4} and show f(X)≠Y; write down the graph Γ_f; and show that changing the codomain to {0,1,4} gives a different function. Then decide two non-examples: the reverse rule s(y)='the x in X with x²=y' is not a function Y→X, and g(x)=x+4 is not a function X→Y.

Treats only pure mathematical total functions between the explicit finite sets X and Y (MKO assumptions a1 and a2). Universal statements over finite sets are checked by complete enumeration. It gives no formal definition of partial functions, does not bind the Lean theorem function_total_unique, and does not treat program semantics; it does not change the canonical MKO or its English edition.

Givens and symbols

• function_def
• image_preimage_def
• injective_surjective_def
• cartesian_product_def
• finite_forall

• G1 — X={−2,−1,0,1,2} and Y={0,1,2,3,4,5}, both explicit sets of integers (assumption a1).
• G2 — f:X→Y is given by the rule f(x)=x².
• G3 — Two rules for comparison: s from Y to X, with s(y) 'the x in X such that x²=y'; and g from X to Y, with g(x)=x+4.

• X,\ Y — domain and codomain
• f(X) — range: the set of actual outputs
• \Gamma_f — graph: the set of pairs (x,f(x))
• f_1 — the same rule with codomain {0,1,4}
• s,\ g — two rules to be tested

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.
• 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.
• cartesian_product_def · prerequisite — Cartesian product: A×B is the set of ordered pairs (a,b) with a∈A and b∈B; (a,b)=(c,d) ⇔ a=c and b=d.
• def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv.
• eq_refl_symm_trans · prerequisite — Properties of equality: u=u; if u=v then v=u; if u=v and v=w then u=w.
• 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.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• finite_counting_basics · prerequisite — Finite counting: for disjoint finite sets A, B, |A∪B|=|A|+|B|; |A×B|=|A|·|B|; there is a bijection between finite sets ⇔ they have the same number of elements.
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• mko_function_def · cited — A function f:X→Y assigns exactly one output in Y to every input in X; the codomain Y need not equal the function's actual range. · mko-function-mapping
• finite_forall · prerequisite — Quantifiers over a listed finite set: if X is given by a list, then ∀x∈X, P(x) is equivalent to P holding for each listed element, and ∃x∈X, P(x) to P holding for at least one listed element.
• graph_def · prerequisite — Graph of a function: the graph of f:X→Y is Γ_f={(x,f(x)) ∣ x∈X}, a subset of X×Y.
• L_no_root_2 · lemma — No x in X satisfies x²=2.

Main derivation

\text{rule }x\mapsto x^2

f:X\to Y,\ X=\{-2,-1,0,1,2\},\ Y=\{0,1,2,3,4,5\},\ f(x)=x^2

f:X\to Y\ \text{is a function}

\forall x\in X:\ x^2\in Y\ \land\ \forall y,y'\ (y=x^2\land y'=x^2\Rightarrow y=y')

(-2)^2,\ (-1)^2,\ 0^2,\ 1^2,\ 2^2

4,\ 1,\ 0,\ 1,\ 4

f(x)\in\{4,1,0,1,4\}

\forall x\in X:\ f(x)\in Y

y=x^2,\ y'=x^2

y=y'

\text{existence (S04)},\ \text{uniqueness (S05)}

f:X\to Y\ \text{is a function}

f(X)=\{f(x)\mid x\in X\}

f(X)=\{0,1,4\}

f(X)=\{0,1,4\}\subseteq Y,\ 2\in Y

2\notin f(X),\ f(X)\neq Y

\Gamma_f=\{(x,f(x))\mid x\in X\}

\Gamma_f=\{(-2,4),(-1,1),(0,0),(1,1),(2,4)\}\subseteq X\times Y

f(-1)=1,\ f(1)=1

f(-1)=f(1),\ -1\neq 1:\ f\ \text{not injective}

f_1:X\to\{0,1,4\},\ f_1(x)=x^2

f_1\ \text{is a surjective function},\ f_1\neq f

y=1:\ \{x\in X\mid x^2=1\}

\{-1,1\}:\ \text{two candidate outputs}

y=2:\ \{x\in X\mid x^2=2\}

\varnothing:\ \text{no output}

g(2)=2+4

g(2)=6\notin Y:\ g\ \text{is not a function }X\to Y

f,\ f_1,\ s,\ g

f,f_1\ \text{functions};\ f(X)=\{0,1,4\}\neq Y;\ s,g\ \text{not functions as declared}

Substeps and lemmas

\neg\exists x\in X:\ x^2=2

\forall x\in X:\ x^2\neq 2

x^2\in\{4,1,0,1,4\}\ (x\in X)

\forall x\in X:\ x^2\neq 2

f_1(x)\in\{4,1,0,1,4\}

f_1:X\to\{0,1,4\}\ \text{is a function}

0=f_1(0),\ 1=f_1(1),\ 4=f_1(2)

f_1\ \text{is surjective}

\text{codomain of }f_1=\{0,1,4\},\ \text{codomain of }f=Y

f_1\neq f

Reverse audits

• S15 · sufficient_goal_reduction · S06, S07, S08, S09, S11, S12, S13, S14, and_intro_elim — Goal G is the conjunction of the problem's conclusions; each is proved forwards by the listed steps, and this step only forms the conjunction; G is never used as a premise.
• S14 · premise_audit · mko_function_def, G1, numeric_evaluation — One output outside the codomain is enough to refute g:X→Y; the positive claim for g:X→ℤ only uses closure of the integers under addition.
• S13 · premise_audit · L_no_root_2, mko_function_def — One input without an output is enough; the conclusion depends on the actual contents of X.
• S12 · premise_audit · mko_function_def, S03 — One input violating uniqueness is enough to show the rule is not a function.
• S11.3 · premise_audit · function_def, set_extensionality — This relies on the convention that the codomain is part of a function's data (function_def, consistent with the MKO); if a function were identified with its graph alone, f and f₁ would count as equal, and this guide does not adopt that convention.
• S11.2 · premise_audit · injective_surjective_def, finite_forall — A preimage is given for each of the three elements of the codomain, a complete check.
• S11.1 · premise_audit · S03, S05, finite_forall, mko_function_def — Every output must lie in the new codomain; this is a complete check over X.
• S11 · premise_audit · function_def, injective_surjective_def — Each of the three sub-conclusions is given by one sub-step; it is not claimed that f₁ is injective (f₁(−1)=f₁(1)).
• S10 · premise_audit · injective_surjective_def, S03 — One counterexample pair refutes injectivity; it is not claimed that this affects whether f is a function (S06 proved that it is).
• S09 · inverse_equivalence · graph_def, finite_forall, set_extensionality — There is one pair for each element of X, so the list and the definition have the same elements, and the step holds both ways.
• S08.2 · premise_audit · S03, finite_forall — All five elements are checked, so the check is complete for X; N6 repeats it over the integers from −2 to 2, which are exactly the elements of X.
• S08.1 · inverse_equivalence · quantifier_negation — Quantifier negation is itself an equivalence, so the step holds both ways.
• S08 · premise_audit · L_no_root_2, set_extensionality, injective_surjective_def — One element of Y outside f(X) is enough to refute f(X)=Y. 2∉f(X) relies on checking every input of X (the lemma); in ℝ, x²=2 has the solution √2, so the conclusion holds only for this X.
• S07 · inverse_equivalence · image_preimage_def, set_extensionality, finite_forall — y∈f(X) ⇔ f(x)=y for some x∈X; comparing the five inputs one by one by finite_forall, both sides have the same elements, so the step holds both ways.
• S06 · sufficient_goal_reduction · S02, S04, S05, mko_function_def — Goal G: f is a function X→Y. Sufficient condition H: existence and uniqueness; H⇒G by S02. H is proved forwards in S04 and S05; G is never used as a premise.
• S05 · premise_audit · eq_refl_symm_trans, forall_intro — Only properties of equality are used; the converse, that different inputs have different outputs, is not claimed, and S10 shows it fails.
• S04 · premise_audit · S03, finite_forall — Enumeration suffices because X consists of exactly these five elements (G1); the converse (every element of Y is an output) is not claimed, and S08 shows it fails.
• S03 · premise_audit · numeric_evaluation, G1 — Each value can be recomputed independently (N1 to N5); X has exactly these five elements, so the computation is complete.
• S02 · inverse_equivalence · mko_function_def, function_def — This unfolds the definition and holds both ways; none of the three requirements (an output exists, it lies in Y, it is unique) may be dropped.
• S01 · premise_audit · G1, G2, def_intro — This step only declares; whether f really is a function X→Y (assumption a2) is checked in S02 to S06 and cannot be presupposed.

Error controls and negative controls

Codomain, range and graph are three different objects

The MKO names the mistake of treating codomain, range and graph as one object. Here the codomain Y={0,1,2,3,4,5} is part of the declaration; the range f(X)={0,1,4} is the set of actual outputs; the graph Γ_f is the subset of X×Y consisting of 5 ordered pairs (S07 to S09). Changing the codomain changes the function (S11) but not the range or the graph.

A program function is not automatically a total mathematical function

The MKO also warns against equating program functions, with side effects or failure states, with pure total mathematical functions. For example, a program that searches −2, −1, 0, 1, 2 in order and returns the first number whose square is y returns −1 for y=1 (the search order replaces uniqueness) and fails for y=2. The program runs, but it does not turn s into a function Y→X (S12, S13); it is a different object, with an added choice rule and undefined at y=2 and elsewhere.

Uniqueness is per input

A common error is to confuse these two conditions: a function requires each input to have only one output (S05), not each output to come from only one input. f(−1)=f(1) does not stop f from being a function (S10); conversely, s violates the definition because the input y=1 has two outputs (S12).

• The codomain of f is {0,1,4} → reject — The declared codomain is Y={0,1,2,3,4,5}; {0,1,4} is the range (S07, S08).
• f(−1)=f(1), so f is not a function → reject — A function only needs each input's output to be unique; f is merely not injective (S06, S10).
• s(y)='the x in X with x²=y' defines a function Y→X → reject — y=1 has the two candidates −1 and 1, and y=2 has none (S12, S13).
• g(x)=x+4 is a function X→Y → reject — g(2)=6∉Y (S14).
• f and f₁ have the same graph, so f=f₁ → reject — Their codomains differ (2∈Y but 2∉{0,1,4}), so by function_def they are different (S11.3).

Result and limitations

f:X→Y, f(x)=x², is a function: each input has exactly one output in Y. Its range is {0,1,4}, which is not the codomain Y={0,1,2,3,4,5} (2∉f(X)), and its graph is {(−2,4),(−1,1),(0,0),(1,1),(2,4)}; codomain, range and graph are three different objects. Changing the codomain to {0,1,4} gives a different function f₁, which is surjective. The reverse rule s has two candidates at y=1 and no output at y=2, so it is not a function; g(x)=x+4 is not a function X→Y because g(2)=6∉Y.

• N6 checks x²≠2 at the integers from −2 to 2; these five integers are exactly the elements of X, so it is a complete check for X, but it says nothing about other sets (for example ℝ, where √2 is a solution).
• This guide adopts the convention that the codomain is part of a function's data (function_def, consistent with the MKO); texts that define a function as its graph would judge f=f₁ differently.

Verification and source binding

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

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

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