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

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

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

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

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

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

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

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

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

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

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

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

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

f\ \text{injective}

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

f\ \text{injective but not surjective}

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

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

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

g\ \text{not injective}

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

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

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

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

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

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

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

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

f_0:\varnothing\to B

f_0\ \text{injective}

\text{S01 to S14}

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

Substeps and lemmas

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

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

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

x=x'

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

x=y

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 hit

One 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 first

Another 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 set

One 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)