Surjectivity and codomain coverage: range, preimages and changing the codomain

Goal and scope

Let A={1,2,3,4,5}, B={1,2,3} and the function table f: (1,2),(2,1),(3,3),(4,2),(5,1). Confirm f is a total function A→B, find the range f[A] and the preimages, decide whether f is surjective and find the first preimage of t=2; then replace the codomain by B2={1,2,3,4} and by B3={1,2}, deciding legality and surjectivity; finally treat ∅→∅ and ∅→{7}.

Works inside the MKO's scope: an explicit domain, codomain and finite total function table. Proves two small general lemmas (f[A]⊆B; f surjective ⇔ f[A]=B), decides this example by a complete check, and shows when a change of codomain is legitimate. Results concern this table only and are not extended to other functions; the canonical MKO and its English edition are not changed.

Givens and symbols

• function_def
• image_preimage_def
• set_extensionality
• exists_intro
• numeric_evaluation
• table_function

• G1 — Domain A={1,2,3,4,5}, declared codomain B={1,2,3}.
• G2 — Function table f: (1,2),(2,1),(3,3),(4,2),(5,1) (each row is (input, output)).
• G3 — Replacement codomains B2={1,2,3,4} and B3={1,2}; the target t=2; and the empty functions ∅→∅ and ∅→{7}.

• f[A] — the attained range {f(x) ∣ x∈A}
• B,\ B2,\ B3 — the declared codomain and two replacement codomains
• f^{-1}(\{t\}) — the preimage set {x∈A ∣ f(x)=t} of t
• B\setminus f[A] — the uncovered targets
• f_2 — the same table with codomain B2

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.
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B).
• 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.
• 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.
• 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.
• 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.
• 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.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_surjective_def · cited — A total function f:A→B is surjective exactly when, for every b∈B, there exists x∈A with f(x)=b; equivalently, the attained range f[A] equals the declared codomain B. Surjectivity does not require a unique preimage. · mko-surjective
• 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.
• 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.
• empty_set_def · prerequisite — Empty set: for every x, x∉∅.
• least_element · prerequisite — A nonempty finite set of integers has a unique least element (found by comparing elements). The MKO's 'first preimage' is the numerically least element of the preimage set; if the preimage set is empty the answer is 'none'.
• L_range_sub · lemma — For every total function f:A→B, f[A]⊆B.
• L_surj_range · lemma — For a total function f:A→B: f is surjective ⇔ f[A]=B.

Main derivation

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

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

f[A]=\{f(x)\mid x\in A\}

\{2,1,3,2,1\}=\{1,2,3\}

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

f[A]\subseteq B

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

f^{-1}(\{1\})=\{2,5\},\ f^{-1}(\{2\})=\{1,4\},\ f^{-1}(\{3\})=\{3\}

b\in B=\{1,2,3\}

\forall b\in B\ \exists x\in A:\ f(x)=b

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

f\ \text{surjective}

f(1)=f(4)=2,\ 1\neq 4

f\ \text{not injective, still surjective}

f^{-1}(\{2\})=\{1,4\}

\text{first preimage of}\ 2=\min\{1,4\}=1

f[A]=\{1,2,3\},\ B2=\{1,2,3,4\}

f[A]\subseteq B2,\ \text{so}\ f_2:A\to B2\ \text{is a total function}

B2\setminus f[A]

\{4\}\neq\varnothing,\ f_2^{-1}(\{4\})=\varnothing,\ f_2\ \text{not surjective}

f(3)=3,\ B3=\{1,2\}

3\notin B3,\ \text{so the table is not a function}\ A\to B3

\varnothing\to\varnothing

\text{surjective}

\varnothing\to\{7\}

\neg\exists x\in\varnothing:\ f(x)=7,\ \text{not surjective}

\text{S01 to S13}

f\ \text{surjective};\ f_2\ \text{not};\ B3\ \text{illegal};\ \varnothing\to\varnothing\ \text{surjective};\ \varnothing\to\{7\}\ \text{not}

Substeps and lemmas

y\in f[A]

y\in B

f\ \text{surjective}

f[A]=B

f[A]=B

f\ \text{surjective}

Reverse audits

• S14 · sufficient_goal_reduction · S05, S06, S08, S10, S11, S12, S13, 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.
• S13 · premise_audit · empty_set_def, quantifier_negation — One uncovered target suffices; the difference from S12 is whether the codomain is empty.
• S12 · premise_audit · empty_set_def, forall_intro — Vacuous truth: the codomain has no element that needs covering.
• S11 · premise_audit · table_function — One output outside B3 suffices to refute legitimacy.
• S10 · premise_audit · L_surj_range, S09, numeric_evaluation — One uncovered target suffices to refute surjectivity (N6: |B2|−|f[A]|=1).
• S09 · premise_audit · table_function, subset_def — Legitimacy only requires f[A]⊆B2; it says nothing about surjectivity.
• S08 · premise_audit · least_element, S04 — The preimage set must be complete (S04 checked every input) and nonempty.
• S07 · premise_audit · injective_surjective_def, S05 — One collision refutes injectivity; the surjectivity verdict comes from S05 and is unaffected.
• S06.2 · premise_audit · image_preimage_def, forall_intro — b is arbitrary, so ∀-introduction gives the conclusion for every b.
• S06.1 · premise_audit · mko_surjective_def, L_range_sub, set_extensionality — This is the '⇒' direction of the lemma; neither inclusion may be dropped.
• S06 · premise_audit · L_surj_range, S02 — Both directions of the lemma are proved in S06.1 and S06.2; this route does not rely on S05.
• S05 · premise_audit · S04, exists_intro, case_analysis, roster_membership, forall_intro — Every element of B must be checked; each b needs one witness, not a unique one.
• S04 · premise_audit · image_preimage_def, S01 — All five inputs must be checked; the sizes summing to |A| is a consistency check.
• S03.1 · premise_audit · function_def, image_preimage_def, subset_def — It needs f to be a function into B; the reverse inclusion B⊆f[A] fails in general and is not claimed.
• S03 · premise_audit · L_range_sub — The lemma is proved in S03.1; it gives one inclusion only.
• S02 · inverse_equivalence · image_preimage_def, set_extensionality — Both descriptions have the same elements, so by set equality it holds both ways.
• S01 · premise_audit · table_function — Surjectivity is meaningful only for a total function; all three qualification conditions are checked.

Error controls and negative controls

The range is not automatically the codomain

One misconception named by the MKO is taking the range to be the codomain automatically. The same table always has range {1,2,3}; with codomain B it is surjective, with codomain B2={1,2,3,4} it is not (S10). Surjectivity compares the range with the declared codomain, so the codomain must be stated first.

Several preimages do not refute surjectivity

Another misconception identified in the MKO is refuting surjectivity with several preimages. 2 has two preimages, 1 and 4, and 1 has two, 2 and 5; this makes f non-injective (S07), but surjectivity only requires at least one preimage per target (S05).

A new codomain must keep every output

MKO assumption a2: a replacement codomain must contain every existing output. B3={1,2} drops the output 3, which still occurs, so the table is not a function A→B3 (S11); shrinking the codomain cannot be used to 'make it surjective'.

• f is not surjective, because 2 has two preimages, 1 and 4 → reject — Surjectivity only requires at least one preimage per target; 1, 2 and 3 all have one.
• f₂:A→{1,2,3,4} is surjective, because its range {1,2,3} is the codomain → reject — The declared codomain is B2={1,2,3,4}, and 4 has no preimage.
• After changing the codomain to {1,2}, f becomes surjective → reject — f(3)=3∉{1,2}, so the table is no longer a total function and the surjectivity question does not apply.
• The empty function ∅→{7} is surjective, since no counterexample can be found → reject — 7 needs some x∈∅ as a preimage, but ∅ has no elements; 7 itself is an uncovered target.
• The first preimage of t=2 is 4 → reject — The preimage set is {1,4}, and its numerically least element is 1.

Result and limitations

f: (1,2),(2,1),(3,3),(4,2),(5,1) is a total function A→B with f[A]={1,2,3}=B, so f is surjective; it is not injective (f(1)=f(4)=2), but several preimages do not affect surjectivity. The preimages of t=2 are {1,4}, and the first is 1. With codomain B2={1,2,3,4} the same table is still legitimate but 4 has no preimage, so it is not surjective; with B3={1,2} it is illegitimate, because f(3)=3∉B3. ∅→∅ is surjective and ∅→{7} is not.

• N3 and N4 encode 'a number equals none of the listed values' as a nonzero product of differences (zero-product property); they only recompute these particular numbers.
• This guide does not prove counting facts such as 'a surjection between finite sets needs |A|≥|B|', and does not treat infinite domains.

Verification and source binding

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

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

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