# Injectivity and distinct inputs: table qualification, collision witnesses and fibers

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

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-injective-01 · production-20261019-adopted-96



## Goal and scope

Let A={1,2,3,4}, B={1,2,3,4,5,6}, with function tables f: (1,4),(2,6),(3,1),(4,5); g: (1,4),(2,6),(2,6),(3,4),(4,6); h: (1,4),(2,6),(2,5),(3,1),(4,5). Decide which tables are total functions A→B; decide whether f and g are injective and list their fibers; find g's first collision in lexicographic order; decide whether g restricted to C={1,2} is injective; and treat the empty domain.

Works inside the MKO's scope: finite integer-labelled function tables. First checks total-function qualification, then decides injectivity by complete comparison, and proves two small general lemmas (comparing input pairs x<y suffices; injectivity is equivalent to every fiber having at most one element). Results concern these tables only and are not extended to other functions; infinite domains are not treated; the canonical MKO and its English edition are not changed.





## Givens and symbols


- function_def
- image_preimage_def
- contrapositive
- quantifier_negation
- numeric_evaluation
- table_function


- G1 — A={1,2,3,4}, B={1,2,3,4,5,6}.
- G2 — Function tables (each row is (input, output)): f: (1,4),(2,6),(3,1),(4,5); g: (1,4),(2,6),(2,6),(3,4),(4,6); h: (1,4),(2,6),(2,5),(3,1),(4,5).
- G3 — C={1,2}⊆A; also consider the function f₀:∅→B with empty domain.


- f,\ g,\ h — the three function tables
- f^{-1}(\{b\}) — the fiber {x∈A ∣ f(x)=b} of b
- g|_C — the restriction of g to C
- (x,x') — a collision pair: x<x′ and g(x)=g(x′)
- \varnothing\to B — the function with empty domain





## 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.
- contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
- quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
- 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.
- 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.
- 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.
- 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_injective_def · cited — A total function f:A→B is injective if, for all x,y∈A, f(x)=f(y) implies x=y. Equivalently, distinct inputs have distinct outputs. Every fiber {x∈A:f(x)=b}, for b∈B, has at most one element. · mko-injective
- table_function · prerequisite — A finite table of rows (x,y) defines a total function A→B exactly when every row has x∈A and y∈B, every x∈A occurs in at least one row, and rows with the same x have the same output. Identical rows are just repeated listings of the same ordered pair.
- roster_membership · prerequisite — Membership in a listed set: for a finite set given by listing, S={s_i ∣ 1≤i≤n}, z∈S exactly when z=s_i for some i.
- restriction_def · prerequisite — For C⊆A, the restriction f|_C:C→B is defined by f|_C(x)=f(x) for x∈C.
- lex_order · prerequisite — Lexicographic order on integer pairs: (x,x′) comes before (y,y′) exactly when x<y, or x=y and x′<y′.
- empty_set_def · prerequisite — Empty set: for every x, x∉∅.
- L_pairs_lt · lemma — For A⊆ℤ and a function f:A→B: f is injective ⇔ f(x)≠f(y) for all x, y∈A with x<y.
- L_fiber · lemma — For a function f:A→B: f is injective ⇔ for every b∈B the fiber f⁻¹({b}) has at most one element.





## Main derivation

S01 · impliesBefore

f:\ (1,4),(2,6),(3,1),(4,5)

After

f:A\to B\ \text{total};\ f(1)=4,\ f(2)=6,\ f(3)=1,\ f(4)=5

Conditions: none

Rule: table_function · Uses: G1, G2, table_function

Leaf basis: table_function + roster_membership

MKO paragraph one: first check that the table is total on A. Each of the four inputs 1, 2, 3, 4 occurs in exactly one row, the outputs 4, 6, 1, 5 are in B, and no input is paired with two different outputs. So f is a total function A→B.



S02 · equivalentBefore

\forall x,y\in A:\ f(x)=f(y)\Rightarrow x=y

After

\forall x,y\in A:\ x\neq y\Rightarrow f(x)\neq f(y)

Conditions: none

Rule: contrapositive · Uses: mko_injective_def, contrapositive

Leaf basis: mko_injective_def + contrapositive

By the MKO's definition, injective means 'f(x)=f(y) implies x=y'. Taking the contrapositive for each pair x, y gives 'x≠y implies f(x)≠f(y)': distinct inputs have distinct outputs. This form is used for the pairwise comparison below.



S03 · equivalentBefore

\forall x,y\in A:\ x\neq y\Rightarrow f(x)\neq f(y)

After

\forall x,y\in A:\ x<y\Rightarrow f(x)\neq f(y)

Conditions: A\subseteq\mathbb{Z}

Rule: L_pairs_lt · Uses: S02, L_pairs_lt

Leaf basis: case_analysis + order_basics

By Lemma L_pairs_lt, only input pairs with x<y need comparing; A has C(4,2)=6 such pairs (N2). The case x=y needs no comparison, and the case x>y repeats the case y<x.



S04 · impliesBefore

(1,2),(1,3),(1,4),(2,3),(2,4),(3,4)

After

4\neq 6,\ 4\neq 1,\ 4\neq 5,\ 6\neq 1,\ 6\neq 5,\ 1\neq 5;\ f\ \text{injective}

Conditions: none

Rule: forall_intro · Uses: S01, S03, forall_intro

Leaf basis: case_analysis + roster_membership + numeric_evaluation + forall_intro

Compare the outputs of the six input pairs: f(1)=4 differs from f(2)=6, f(3)=1 and f(4)=5; f(2)=6 differs from f(3)=1 and f(4)=5; f(3)=1 differs from f(4)=5. Every pair with x<y has different outputs (N1 checks this as a nonzero product of differences); this is a complete check of the finite A, so by S03 f is injective.



S05 · impliesBefore

f^{-1}(\{b\})=\{x\in A\mid f(x)=b\},\ b\in B

After

\{3\},\ \varnothing,\ \varnothing,\ \{1\},\ \{4\},\ \{2\}\quad(b=1,2,3,4,5,6)

Conditions: none

Rule: image_preimage_def · Uses: S01, image_preimage_def

Leaf basis: image_preimage_def + roster_membership + numeric_evaluation

List the fiber of each b in B: for b=1 only f(3)=1, so the fiber is {3}; for b=2 and 3 no input maps there, so the fibers are empty; b=4 gives {1}; b=5 gives {4}; b=6 gives {2}. Every fiber has at most one element; the fiber sizes sum to 1+0+0+1+1+1=4=|A| (N8), since every input lies in exactly one fiber.



S06 · theorem_applicationBefore

|f^{-1}(\{b\})|\le 1\ \text{for all}\ b\in B

After

f\ \text{injective}

Conditions: none

Rule: L_fiber · Uses: S04, S05, L_fiber

Leaf basis: image_preimage_def + eq_refl_symm_trans + mko_injective_def

By Lemma L_fiber, 'every fiber has at most one element' is equivalent to injectivity. The fibers in S05 all have at most one element, so the fiber view also gives that f is injective, in agreement with the pairwise comparison of S04. This is the fiber form stated in the MKO.



S07 · impliesBefore

f^{-1}(\{2\})=f^{-1}(\{3\})=\varnothing

After

f\ \text{injective but not surjective}

Conditions: none

Rule: injective_surjective_def · Uses: S05, S04, injective_surjective_def

Leaf basis: injective_surjective_def + image_preimage_def

The codomain elements 2 and 3 have empty fibers and no preimage, so f is not surjective; yet f is still injective (S04, S06). MKO paragraph two: an injection may miss codomain elements, and fiber sizes may be zero or one.



S08 · impliesBefore

g:\ (1,4),(2,6),(2,6),(3,4),(4,6)

After

g:A\to B\ \text{total};\ g(1)=4,\ g(2)=6,\ g(3)=4,\ g(4)=6

Conditions: none

Rule: table_function · Uses: G1, G2, table_function

Leaf basis: table_function + roster_membership

The table of g lists (2,6) twice. The two rows are identical, a repeated listing of the same ordered pair (MKO paragraph one), not an input paired with different outputs. Each of the four inputs has a unique output in B, so g is a total function A→B.



S09 · impliesBefore

g(1)=4=g(3),\ 1\neq 3

After

g\ \text{not injective}

Conditions: none

Rule: quantifier_negation · Uses: S08, mko_injective_def, quantifier_negation

Leaf basis: quantifier_negation + exists_intro + mko_injective_def

The negation of injectivity (quantifier negation together with ¬(P⇒Q) ⇔ P∧¬Q) is: there exist x, y∈A with g(x)=g(y) and x≠y. Take x=1 and y=3: g(1)=g(3)=4 (N3) while 1≠3. This collision witness alone shows that g is not injective.



S10 · impliesBefore

\{(x,x')\mid x<x',\ g(x)=g(x')\}

After

\{(1,3),(2,4)\},\ \text{first}=(1,3)

Conditions: none

Rule: lex_order · Uses: S08, lex_order

Leaf basis: lex_order + case_analysis + numeric_evaluation

MKO paragraph three: for the first finite collision take x<x′ and choose the first pair (x,x′) in lexicographic order. Compare the six pairs: (1,2): 4 and 6 differ; (1,3): 4=4, a collision; (1,4): 4 and 6 differ; (2,3): 6 and 4 differ; (2,4): 6=6, a collision; (3,4): 4 and 6 differ (N4, N5). The collision set is {(1,3),(2,4)}; since 1<2, the first pair in lexicographic order is (1,3).



S11 · impliesBefore

g^{-1}(\{b\}),\ b\in B

After

g^{-1}(\{4\})=\{1,3\},\ g^{-1}(\{6\})=\{2,4\},\ \text{others}\ \varnothing

Conditions: none

Rule: image_preimage_def · Uses: S08, image_preimage_def, L_fiber

Leaf basis: image_preimage_def + roster_membership + numeric_evaluation

The fibers of g: the fiber of 4 is {1,3}, the fiber of 6 is {2,4}, and the fibers of b=1, 2, 3, 5 are empty. The sizes sum to 0+0+0+2+0+2=4=|A| (N9). Two fibers have two elements, so by L_fiber g is again seen not to be injective; each fiber of size 2 corresponds to one collision.



S12 · impliesBefore

g|_C,\ C=\{1,2\}

After

g|_C(1)=4\neq 6=g|_C(2),\ g|_C\ \text{injective}

Conditions: none

Rule: restriction_def · Uses: S08, G3, restriction_def, L_pairs_lt

Leaf basis: restriction_def + case_analysis + numeric_evaluation

Restrict to C={1,2}: g|_C(1)=4 and g|_C(2)=6. The only pair x<y in C is (1,2), and 4≠6 (N6), so by L_pairs_lt g|_C is injective. MKO paragraph three: after restriction only inputs in C are compared, so a non-injective function can have an injective restriction; both collisions (1,3) and (2,4) have at least one input outside C.



S13 · impliesBefore

h:\ (2,6),\ (2,5)

After

h\ \text{is not a function}\ A\to B

Conditions: none

Rule: table_function · Uses: G2, table_function

Leaf basis: table_function + numeric_evaluation

In the table of h the input 2 occurs in the rows (2,6) and (2,5), with outputs 6≠5 (N7). One input paired with different outputs means h is not a function (MKO paragraph one). Injectivity is defined for total functions, so the question whether h is injective does not apply; the correct verdict is 'not a function', not 'not injective'.



S14 · impliesBefore

f_0:\varnothing\to B

After

f_0\ \text{injective}

Conditions: none

Rule: forall_intro · Uses: G3, mko_injective_def, empty_set_def, forall_intro

Leaf basis: empty_set_def + forall_intro + mko_injective_def

With empty domain, the injectivity condition is ∀x,y∈∅ (f₀(x)=f₀(y)⇒x=y). For any x, x∈∅ is false, and an implication with a false antecedent is true, so the condition holds for every x, y; by ∀-introduction f₀ is injective (MKO assumption a2: injectivity holds for an empty domain).



S15 · impliesBefore

\text{S01 to S14}

After

f\ \text{injective};\ g\ \text{not, first collision}\ (1,3);\ g|_C\ \text{injective};\ h\ \text{not a function};\ f_0\ \text{injective}

Conditions: none

Rule: and_intro_elim · Uses: S01, S04, S07, S08, S09, S10, S12, S13, S14

Leaf basis: and_intro_elim

Summary: f is a total function and injective, with every fiber of size at most one, though 2 and 3 have no preimage (S04 to S07); g is a total function (the repeated row is harmless) and not injective, with collisions (1,3) and (2,4) and first collision (1,3) (S08 to S11); g|_C is injective (S12); h is not a function (S13); f₀:∅→B is injective (S14).







## Substeps and lemmas

S03.1 · equivalentBefore

\forall x<y:\ f(x)\neq f(y)

After

\forall x\neq y:\ f(x)\neq f(y)

Conditions: A\subseteq\mathbb{Z}

Rule: case_analysis · Uses: case_analysis, order_basics

Leaf basis: case_analysis + order_basics + eq_refl_symm_trans

⇐: x<y implies x≠y, so the right-hand form gives the left. ⇒: let x≠y. By trichotomy, x<y or y<x. If x<y, f(x)≠f(y) directly; if y<x, f(y)≠f(x), and '≠' is symmetric. The two cases cover every possibility with x≠y. This proves Lemma L_pairs_lt (together with S02).



S06.1 · impliesBefore

f\ \text{injective},\ x,x'\in f^{-1}(\{b\})

After

x=x'

Conditions: none

Rule: mko_injective_def · Uses: mko_injective_def, image_preimage_def

Leaf basis: mko_injective_def + image_preimage_def + eq_refl_symm_trans

⇒: let f be injective and x, x′ both lie in the fiber of b. Then f(x)=b=f(x′), so f(x)=f(x′) by symmetry and transitivity of equality, and injectivity gives x=x′. So any two elements of the fiber coincide: it has at most one element.



S06.2 · impliesBefore

|f^{-1}(\{b\})|\le 1\ \forall b,\ f(x)=f(y)

After

x=y

Conditions: none

Rule: image_preimage_def · Uses: image_preimage_def

Leaf basis: image_preimage_def + forall_intro + eq_refl_symm_trans

⇐: suppose every fiber has at most one element and f(x)=f(y). Let b=f(x); then x and y both lie in the fiber of b, which has at most one element, so x=y. This is the definition of injectivity. S06.1 and S06.2 prove Lemma L_fiber.







## Reverse audits


- S15 · sufficient_goal_reduction · S04, S07, S10, S12, S13, S14, and_intro_elim — Goal G: the verdicts the task asks for. Sufficient condition H: the conclusions of the listed steps; H⇒G is just conjunction, H is proved forwards from G1 to G3, and G is never used as a premise.
- S14 · premise_audit · empty_set_def, forall_intro — Vacuous truth: there are no inputs, so there is no collision to refute injectivity.
- S13 · premise_audit · table_function — One input with two different outputs suffices to refute function status.
- S12 · premise_audit · restriction_def, L_pairs_lt — All input pairs in C must be listed (there is one); it is not claimed that g itself is therefore injective.
- S11 · premise_audit · image_preimage_def, L_fiber — One fiber of size above 1 is enough to refute injectivity; the full list is for comparison with S10.
- S10 · premise_audit · lex_order, S08, numeric_evaluation — This guide's audit compares all 6 pairs, lists every collision and takes the lexicographically least. Mathematically, an ordered scan may instead stop at its first collision after excluding every earlier pair. Finding an arbitrary collision without excluding earlier ones is insufficient. The prescribed full enumeration is unchanged.
- S09 · premise_audit · quantifier_negation, exists_intro, S08 — One collision witness suffices; it must consist of two different inputs from A.
- S08 · premise_audit · table_function — The repeated row is harmless only because its outputs agree; with different outputs the table would fail to be a function, as h does (S13).
- S07 · premise_audit · injective_surjective_def, S05 — One codomain element without a preimage suffices to refute surjectivity; this does not affect the verdict on injectivity.
- S06.2 · premise_audit · image_preimage_def, forall_intro — x and y are arbitrary, so ∀-introduction gives the conclusion for all x, y.
- S06.1 · premise_audit · mko_injective_def, image_preimage_def, eq_refl_symm_trans — This is the '⇒' direction of the lemma; the converse is S06.2.
- S06 · premise_audit · L_fiber, S05 — The lemma is proved in S06.1 and S06.2; this step is a second, independent route that does not rely on S04.
- S05 · premise_audit · image_preimage_def, S01 — All six elements of B must be listed; the fiber sizes summing to |A| is a consistency check.
- S04 · premise_audit · S03, case_analysis, numeric_evaluation — All 6 pairs must be compared; missing one would block the conclusion. The verdict concerns f only and is not extended to other functions.
- S03.1 · inverse_equivalence · case_analysis, order_basics, eq_refl_symm_trans — Both directions have reasons; the elements of A must be comparable (integer labels).
- S03 · inverse_equivalence · L_pairs_lt — Both directions of the lemma are proved in S03.1.
- S02 · inverse_equivalence · contrapositive — A statement and its contrapositive are equivalent, both ways, for each pair.
- S01 · premise_audit · table_function, G1, G2 — All three conditions (inputs and outputs in range, every input present, outputs unique) must be checked; injectivity only makes sense for tables that pass this step.





## Error controls and negative controls

Injectivity does not require every codomain element to be hitOne misconception named by the MKO is thinking injectivity means every codomain element has a preimage. The codomain elements 2 and 3 of f have no preimage (S07), yet f is injective; 'every codomain element has a preimage' is the condition for surjectivity. Injectivity only requires fibers of size at most one, and zero is allowed.

Check total-function qualification firstAnother misconception identified in the MKO is skipping total-function qualification. h sends input 2 to both 6 and 5, so it is not a function (S13), and one cannot say 'h is not injective'; whereas g's repeated listing of (2,6) does not break function status (S08). Checks like S01 and S08 must come before any injectivity verdict.

This guide chooses the first collision from the complete collision setOne collision witness is enough to refute injectivity (S09), but this guide audits the 'first collision' by listing all collision pairs with x<x′ and taking the lexicographically least; an ordered scan can also stop after excluding every earlier pair (S10). Grabbing (2,4) and calling it the first would miss (1,3), which comes earlier.


- f is not injective, because the codomain element 2 has no preimage → reject — A missing preimage concerns surjectivity; for each of the six distinct-input pairs, the two f-values differ, so f is injective.
- h is not injective, because h(2) has two values → reject — h is not a function at all; the injectivity question does not apply, and the correct verdict is 'not a function'.
- The table of g lists (2,6) twice, so g is not a function → reject — The two rows are identical, a repeated listing of one ordered pair; g is a total function.
- g is not injective, so g restricted to C={1,2} is not injective either → reject — g|_C(1)=4≠6=g|_C(2), so the restriction is injective.
- The first collision of g is (2,4) → reject — The complete collision set is {(1,3),(2,4)}, and the first in lexicographic order is (1,3).





## Result and limitations

f: (1,4),(2,6),(3,1),(4,5) is a total function and injective: the two outputs differ for each of the six distinct-input pairs and every fiber has at most one element; it is not surjective (2 and 3 have no preimage). g is a total function (the repeated (2,6) is harmless) but not injective; its collision pairs are (1,3) and (2,4), and the first in lexicographic order is (1,3); g restricted to {1,2} is injective. h gives input 2 two outputs, so it is not a function and the injectivity question does not apply. The function with empty domain is injective.


- N1 and N5 encode 'the listed pairs all have different outputs' as a nonzero product of differences (zero-product property); they only recompute these particular numbers.
- This guide treats finite integer-labelled tables only; L_pairs_lt needs a domain whose elements can be compared, and for general sets the form in S02 should be used directly.





## Verification and source binding

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: dafc9b0a4b50798ff78dcf28638ea8cdec7b99bc6437f143ac45ff1db55d4b0b
- original source SHA-256: 2abb8f0cb47a609b84f38055e37ace578fef639ffbc99b0a564f7e91305f5af8
- 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-injective-01.json)