# Function mapping: deciding whether a rule is a function, and separating codomain, range and graph [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-function-mapping/) 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-function-mapping-01 · production-20261019-adopted-96 ## 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 S01 · definitionBefore \text{rule }x\mapsto x^2 After f:X\to Y,\ X=\{-2,-1,0,1,2\},\ Y=\{0,1,2,3,4,5\},\ f(x)=x^2 Conditions: none Rule: def_intro · Uses: G1, G2 Leaf basis: def_intro + mko_function_def Declaring f:X→Y supplies three pieces of data: the domain X, the codomain Y, and the rule x↦x². By the MKO, the core of a function is the rule that every allowed input has exactly one output, not a drawn curve; X and Y are explicit sets (assumption a1). S02 · equivalentBefore f:X\to Y\ \text{is a function} After \forall x\in X:\ x^2\in Y\ \land\ \forall y,y'\ (y=x^2\land y'=x^2\Rightarrow y=y') Conditions: none Rule: mko_function_def · Uses: S01, mko_function_def Leaf basis: mko_function_def + function_def + def_unfold By the MKO's definition, f:X→Y is a function exactly when every input in X has an output in Y (existence) and only one (uniqueness). For the rule x↦x², existence means x²∈Y, and uniqueness means that if y and y′ both equal x², then y=y′. S03 · impliesBefore (-2)^2,\ (-1)^2,\ 0^2,\ 1^2,\ 2^2 After 4,\ 1,\ 0,\ 1,\ 4 Conditions: none Rule: numeric_evaluation · Uses: G1, G2 Leaf basis: numeric_evaluation + neg_mul Square each of the five inputs of X: (−2)²=4, (−1)²=1, 0²=0, 1²=1, 2²=4. The square of a negative number is positive, so −2 and 2 give the same value. S04 · impliesBefore f(x)\in\{4,1,0,1,4\} After \forall x\in X:\ f(x)\in Y Conditions: none Rule: finite_forall · Uses: S03, G1 Leaf basis: finite_forall + numeric_evaluation 4, 1 and 0 all appear in the list Y={0,1,2,3,4,5}. X is a finite list and all five inputs have been checked, so by finite_forall every input has an output in Y. This is an exhaustive check of all of X, not a sample; for an infinite X a general argument would be needed. S05 · impliesBefore y=x^2,\ y'=x^2 After y=y' Conditions: none Rule: eq_refl_symm_trans · Uses: S02 Leaf basis: eq_refl_symm_trans + forall_intro Suppose that for the same x, both y and y′ are outputs of f, that is y=x² and y′=x². By symmetry and transitivity of equality, y=y′. x² is a definite number determined by x, so one input cannot have two different outputs. This argument holds for every x without a case-by-case check. S06 · impliesBefore \text{existence (S04)},\ \text{uniqueness (S05)} After f:X\to Y\ \text{is a function} Conditions: none Rule: mko_function_def · Uses: S02, S04, S05 Leaf basis: mko_function_def + and_intro_elim Existence (S04) and uniqueness (S05) both hold, so by the equivalence S02, f:X→Y is a function, satisfying assumption a2. S07 · equivalentBefore f(X)=\{f(x)\mid x\in X\} After f(X)=\{0,1,4\} Conditions: none Rule: image_preimage_def · Uses: S03, S06 Leaf basis: image_preimage_def + finite_forall + set_extensionality The range (image) is the set of actual outputs f(X)={f(x) ∣ x∈X}. By S03 the outputs are 4, 1, 0, 1, 4 in order; repeated outputs count once in a set, so f(X)={0,1,4}. S08 · impliesBefore f(X)=\{0,1,4\}\subseteq Y,\ 2\in Y After 2\notin f(X),\ f(X)\neq Y Conditions: none Rule: L_no_root_2 · Uses: S04, S07 Leaf basis: quantifier_negation + finite_forall + set_extensionality + injective_surjective_def f(X)⊆Y (every output is in Y, S04). By Lemma L_no_root_2 (proved in S08.1 and S08.2), no x in X has x²=2, so 2∉f(X); but 2∈Y. Hence f(X)≠Y: the codomain is not the range, and f:X→Y is not surjective. This is the MKO's point that the codomain Y need not equal the actual range. Likewise 3 and 5 are not in f(X). S09 · equivalentBefore \Gamma_f=\{(x,f(x))\mid x\in X\} After \Gamma_f=\{(-2,4),(-1,1),(0,0),(1,1),(2,4)\}\subseteq X\times Y Conditions: none Rule: graph_def · Uses: S03, S06 Leaf basis: graph_def + cartesian_product_def + finite_counting_basics + numeric_evaluation By the definition of the graph, substituting the values of S03 gives five ordered pairs. Γ_f is a subset of X×Y: X×Y has 5·6=30 ordered pairs, and Γ_f takes 5 of them, exactly one per input. Compare the three objects: the codomain Y has 6 numbers, the range f(X) has 3 numbers, and the graph Γ_f has 5 ordered pairs. The first two are subsets of Y, the graph is a subset of X×Y; they are different mathematical objects. S10 · impliesBefore f(-1)=1,\ f(1)=1 After f(-1)=f(1),\ -1\neq 1:\ f\ \text{not injective} Conditions: none Rule: injective_surjective_def · Uses: S03 Leaf basis: injective_surjective_def + numeric_evaluation f(−1)=1=f(1) but −1≠1, so f is not injective: different inputs may share an output. This does not violate the definition of a function, which requires each input to have a unique output, not each output to come from a single input. S11 · impliesBefore f_1:X\to\{0,1,4\},\ f_1(x)=x^2 After f_1\ \text{is a surjective function},\ f_1\neq f Conditions: none Rule: function_def · Uses: S03, S05, S08 Leaf basis: function_def + injective_surjective_def + set_extensionality Declare f₁:X→{0,1,4} with the same rule. S11.1 to S11.3 prove that f₁ is a function, that it is surjective, and that f₁≠f. f₁ and f share the rule, the graph and the range and differ only in the codomain; by function_def the codomain is part of the data of a function. S12 · impliesBefore y=1:\ \{x\in X\mid x^2=1\} After \{-1,1\}:\ \text{two candidate outputs} Conditions: none Rule: mko_function_def · Uses: G3, S03 Leaf basis: mko_function_def + finite_forall + numeric_evaluation Consider the reverse rule s: for y∈Y, s(y) is the x in X with x²=y. For y=1, both x=−1 and x=1 qualify (S03), and −1≠1: one input has two candidate outputs, uniqueness fails, so s is not a function Y→X. This is directly linked to the failure of injectivity in S10. S13 · impliesBefore y=2:\ \{x\in X\mid x^2=2\} After \varnothing:\ \text{no output} Conditions: none Rule: mko_function_def · Uses: G3, S08 Leaf basis: mko_function_def + quantifier_negation + finite_forall For y=2, by Lemma L_no_root_2 no x in X has x²=2: this input has no output, so existence fails as well. S12 and S13 each suffice to show that s is not a function Y→X; s commits both errors, 'several outputs' and 'no output'. S14 · impliesBefore g(2)=2+4 After g(2)=6\notin Y:\ g\ \text{is not a function }X\to Y Conditions: none Rule: mko_function_def · Uses: G1, G3 Leaf basis: mko_function_def + numeric_evaluation The rule g(x)=x+4 gives 6 at the input 2, and 6∉Y (the largest element of Y is 5), so the input 2 has no output in Y and g is not a function X→Y. Declared as g:X→ℤ, the same rule gives a unique integer x+4 for every x and is a function. Whether a rule is a function depends on the declared codomain, not only on the formula. S15 · impliesBefore f,\ f_1,\ s,\ g After f,f_1\ \text{functions};\ f(X)=\{0,1,4\}\neq Y;\ s,g\ \text{not functions as declared} Conditions: none Rule: and_intro_elim · Uses: S06, S07, S08, S09, S11, S12, S13, S14 Leaf basis: and_intro_elim Collect the results: f:X→Y is a function (S06); its range {0,1,4} is not the codomain Y (S07, S08); its graph has 5 ordered pairs (S09); changing the codomain gives a different, surjective function f₁ (S11); s is not a function Y→X (S12, S13); g is not a function X→Y (S14). ## Substeps and lemmas S08.1 · equivalentBefore \neg\exists x\in X:\ x^2=2 After \forall x\in X:\ x^2\neq 2 Conditions: none Rule: quantifier_negation · Uses: image_preimage_def Leaf basis: quantifier_negation + image_preimage_def By the definition of image, 2∈f(X) means ∃x∈X, x²=2. By negating the quantifier, 'there is no such x' is equivalent to 'every x∈X has x²≠2'. S08.2 · impliesBefore x^2\in\{4,1,0,1,4\}\ (x\in X) After \forall x\in X:\ x^2\neq 2 Conditions: none Rule: finite_forall · Uses: S03, S08.1 Leaf basis: finite_forall + numeric_evaluation By S03, the squares of the five inputs of X are 4, 1, 0, 1, 4, and none equals 2. By finite_forall, ∀x∈X, x²≠2; by S08.1, no x in X has x²=2. S08.1 and S08.2 together prove Lemma L_no_root_2. S11.1 · impliesBefore f_1(x)\in\{4,1,0,1,4\} After f_1:X\to\{0,1,4\}\ \text{is a function} Conditions: none Rule: finite_forall · Uses: S03, S05 Leaf basis: finite_forall + mko_function_def By S03 all five outputs lie in {0,1,4}, so existence holds by finite_forall; uniqueness is as in S05. So f₁ is a function. S11.2 · impliesBefore 0=f_1(0),\ 1=f_1(1),\ 4=f_1(2) After f_1\ \text{is surjective} Conditions: none Rule: injective_surjective_def · Uses: S03, S11.1 Leaf basis: injective_surjective_def + finite_forall + exists_intro Every element of the codomain {0,1,4} has a preimage: 0=f₁(0), 1=f₁(1), 4=f₁(2). By finite_forall and the definition of surjective, f₁ is surjective. S11.3 · impliesBefore \text{codomain of }f_1=\{0,1,4\},\ \text{codomain of }f=Y After f_1\neq f Conditions: none Rule: function_def · Uses: S08, S11.1 Leaf basis: function_def + set_extensionality 2∈Y but 2∉{0,1,4}, so the two codomains differ. By function_def, equal functions need the same domain, codomain and values at every point, so f₁≠f, even though the two agree at every point. ## 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 objectsThe 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 functionThe 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 inputA 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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-function-mapping-01.json)