Bijectivity: testing given functions by fiber profiles, kept apart from whether some bijection exists

Goal and scope

Let A={1,2,3}, B={4,5,6}, and let f, g:A→B be given by tables: f(1)=5, f(2)=6, f(3)=4; g(1)=4, g(2)=4, g(3)=6. First prove, for any total function, the equivalence: bijective ⇔ the fiber of every b∈B has exactly one element. Then list the complete fiber profiles of f and g in the codomain order 4, 5, 6, and decide that f is bijective while g is neither injective nor surjective. Finally answer the different question of whether some bijection exists: one exists A→B (f is one), none exists {1,2,3}→{4,5}, and ∅→∅ has exactly one, the empty bijection.

The fiber characterization (S03 to S05) is proved for total functions on arbitrary sets; everything else is a finite-set exercise under MKO assumptions a1 and a2. On the existence side, A→B is answered by the explicit witness f, the non-existence for {1,2,3}→{4,5} is proved directly in sub-steps, and the general fact that finite sets admit a bijection exactly when they have the same number of elements is taken from the prerequisite rule finite_counting_basics and not reproved. Infinite cardinalities are not treated; the canonical MKO and its English edition are not changed.

Givens and symbols

• function_def
• injective_surjective_def
• image_preimage_def
• set_builder
• finite_counting_basics
• numeric_evaluation

• G1 — A={1,2,3}, B={4,5,6}; f:A→B is f(1)=5, f(2)=6, f(3)=4.
• G2 — g:A→B is g(1)=4, g(2)=4, g(3)=6; its codomain is still declared to be B={4,5,6}.
• G3 — C={4,5}; question: does a bijection A→C exist?
• G4 — MKO assumption a1: testing a given function and asking whether some bijection exists are distinct questions. a2: existence exercises use finite sets with nonnegative integer sizes; size zero on both sides permits the unique empty bijection.

• f,g:A\to B — the two given total functions
• f^{-1}(\{b\}) — the fiber {a∈A ∣ f(a)=b} of b; the notation does not presuppose that f is invertible
• |S| — the number of elements of a finite set S
• A=\{1,2,3\},\ B=\{4,5,6\},\ C=\{4,5\} — the domain and two codomains
• \varnothing — the empty set

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.
• 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.
• 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_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and 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.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• 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.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• 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_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• 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.
• 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).
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• 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.
• 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.
• mko_bijective_def · cited — A total function f:A→B is bijective exactly when it is both injective and surjective, or equivalently when each fiber of b∈B has exactly one element. For finite sets, some bijection A→B exists exactly when |A|=|B|; equal cardinality does not make every specified f bijective. · mko-bijective
• fiber_def · prerequisite — Fiber: for a function f:A→B and b∈B, the fiber of b is the preimage f^{-1}({b})={a∈A ∣ f(a)=b}; it is defined for every function and may be empty.
• count_maps · prerequisite — Counting (multiplication principle): if |A|=m and |B|=n there are n^m functions A→B; if m=n, exactly n! of them are bijections.
• L_inj_fiber · lemma — For a total function f:A→B: f is injective ⇔ the fiber of every b∈B has at most one element.
• L_surj_fiber · lemma — For a total function f:A→B: f is surjective ⇔ the fiber of every b∈B has at least one element.
• L_no_inj_3_2 · lemma — No function h:{1,2,3}→{4,5} is injective.

Main derivation

f,g\ \text{given by tables on}\ A=\{1,2,3\}

f,g:A\to B\ \text{total functions},\ B=\{4,5,6\}

b\in B

f^{-1}(\{b\})=\{a\in A\mid f(a)=b\}

f\ \text{injective}

\forall b\in B:\ |f^{-1}(\{b\})|\le 1

f\ \text{surjective}

\forall b\in B:\ |f^{-1}(\{b\})|\ge 1

f\ \text{bijective}

\forall b\in B:\ |f^{-1}(\{b\})|=1

f^{-1}(\{4\}),\ f^{-1}(\{5\}),\ f^{-1}(\{6\})

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

|f^{-1}(\{4\})|=|f^{-1}(\{5\})|=|f^{-1}(\{6\})|=1

f\ \text{bijective}

g^{-1}(\{4\}),\ g^{-1}(\{5\}),\ g^{-1}(\{6\})

\{1,2\},\ \varnothing,\ \{3\}

|g^{-1}(\{4\})|=2

g\ \text{not injective}

g^{-1}(\{5\})=\varnothing

g\ \text{not surjective}

|A|=|B|=3,\ g\ \text{not bijective}

\neg\,\forall\varphi:A\to B\ (\varphi\ \text{bijective})

|A|=3,\ |C|=2

\neg\exists h:A\to C\ \text{bijective}

f:A\to B\ \text{bijective}

\exists\varphi:A\to B\ \text{bijective}

|A|=|B|=3

3^3=27\ \text{functions},\ 3!=6\ \text{bijections}

\varnothing\to\varnothing

\varepsilon=\varnothing\ \text{is the unique bijection}\ \varnothing\to\varnothing

\text{S07, S09, S10, S12, S13, S15}

f\ \text{bijective};\ g\ \text{neither};\ \exists\,A\to B;\ \nexists\,A\to C;\ \exists!\,\varnothing\to\varnothing

Substeps and lemmas

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

a=a'

\forall b:\ |f^{-1}(\{b\})|\le 1,\ f(a)=f(a')

a=a'

\exists a\in A:\ f(a)=b

f^{-1}(\{b\})\neq\varnothing

h:\{1,2,3\}\to\{4,5\}

h(1)=h(2)\ \lor\ h(1)\neq h(2)

h(1)\neq h(2),\ h(1),h(2)\in\{4,5\}

\{h(1),h(2)\}=\{4,5\}

h(3)\in\{4,5\}=\{h(1),h(2)\}

h(3)=h(1)\ \lor\ h(3)=h(2)

Reverse audits

• S16 · sufficient_goal_reduction · S07, S09, S10, S12, S13, S15, and_intro_elim — Goal G is the full set of verdicts in the goal. The sufficient condition H is the conjunction of the sub-results, each proved forwards from the givens in earlier steps; H⇒G uses only conjunction introduction and never takes G as a premise.
• S15 · premise_audit · function_def, injective_surjective_def, cartesian_product_def, forall_intro — All conditions are universal statements over the empty set and hold vacuously; uniqueness comes from ∅×∅ having only one subset.
• S14 · premise_audit · count_maps, numeric_evaluation — The counting rule is a prerequisite not proved here; this step is illustrative only, and the main conclusions S07 and S09 to S13 do not depend on it.
• S13 · premise_audit · S07, exists_intro — Existential introduction needs one witness; the reverse (some bijection exists ⇒ every function is bijective) fails, as S11 shows by counterexample.
• S12.3 · premise_audit · injective_surjective_def, case_analysis, forall_intro — Both cases reach the same conclusion and no extra assumption was put on h, so the conclusion generalizes to every h.
• S12.2 · premise_audit · case_analysis, set_extensionality — What is used is that C has only two elements; the two sub-cases exhaust the possible values of h(1). The converse is not needed.
• S12.1 · premise_audit · case_analysis, injective_surjective_def — The two cases, equal or not equal, are complementary and exhaustive; Case 1 is refuted directly by the definition of injective.
• S12 · premise_audit · L_no_inj_3_2, injective_surjective_def — A bijection must be injective; since no h is injective, none is bijective. The step does not claim there is no surjection A→C (for example 1↦4, 2↦5, 3↦5 is one).
• S11 · premise_audit · S09, quantifier_negation, exists_intro — One explicit counterexample suffices to refute a universal claim; the step does not claim that most functions fail to be bijective (that is the count in S14).
• S10 · premise_audit · L_surj_fiber, S08, S01 — The conclusion relies on 5∈B; shrinking the codomain to {4,6} would give a different function and does not affect the verdict for the declared codomain.
• S09 · premise_audit · L_inj_fiber, contrapositive, S08 — One fiber with more than one element suffices to refute injectivity; the step claims nothing about the other fibers.
• S08 · inverse_equivalence · set_builder, set_extensionality, G2 — All three elements of A were checked against each target; the listed elements satisfy the condition and the others do not, so the sets agree element by element.
• S07 · premise_audit · S05, S06, G1 — What is needed is that every target of the codomain was examined; all three elements of B appear in S06, so no target is missed. Only the ⇐ direction of S05 is used here.
• S06 · inverse_equivalence · set_builder, set_extensionality, G1 — Each listed element satisfies f(a)=b and the other two elements of A were checked not to; by extensionality the sets on both sides are the same, so the step holds both ways.
• S05 · inverse_equivalence · S03, S04, and_intro_elim, order_basics — Each conjunct is replaced by an equivalent condition, so the conjunction stays equivalent; for integers, n≤1 and n≥1 ⇔ n=1 holds both ways (antisymmetry and reflexivity).
• S04.1 · inverse_equivalence · set_builder, injective_surjective_def — The membership condition of set-builder notation is itself two-way: an element of the fiber is the required a, and the required a is an element of the fiber.
• S04 · inverse_equivalence · L_surj_fiber — The equivalence of S04.1 holds both ways for each b, and stays two-way after quantifying over all b.
• S03.2 · premise_audit · function_def, set_builder, injective_surjective_def — The key point is that b=f(a) belongs to B, so that the hypothesis about every fiber of b∈B applies; this is guaranteed because f is a total function.
• S03.1 · premise_audit · injective_surjective_def, set_builder, eq_refl_symm_trans — Only the definition of injective and symmetry and transitivity of equality are used; this is one direction, and the converse is proved separately in S03.2.
• S03 · inverse_equivalence · L_inj_fiber — ⇒ is proved in S03.1 and ⇐ in S03.2; both directions have reasons, so this is an equivalence.
• S02 · premise_audit · fiber_def, image_preimage_def — This only names a set that exists for every function; it does not claim that any fiber is nonempty or has one element.
• S01 · premise_audit · G1, G2, function_def — This step only reads the tables and checks the two requirements of a function (every input has a value, and only one); it derives no new fact. Replacing the codomain by the set of values would change the surjectivity verdict later, so the codomain must be the declared one.

Error controls and negative controls

Equal sizes do not make a given function bijective

The misconception identified in the MKO is declaring a given f bijective straight from |A|=|B|. g is a counterexample: |A|=|B|=3, but g(1)=g(2)=4 and 5 has no preimage. Only 6 of the 27 functions A→B are bijections (S14). Equal size answers only whether some bijection exists (S13); a given function must be judged by its fibers.

Checking one condition is not enough

Checking only injectivity or only surjectivity can mislead. k:{1,2}→{4,5,6} with k(1)=4, k(2)=5 is injective, but the fiber of 6 is empty, so it is not surjective. For finite sets of equal size injective and surjective do imply each other, but that is a theorem needing its own proof and may not simply be assumed; it also fails for infinite sets, for example n↦n+1 on ℕ is injective but not surjective. This guide checks both conditions for f through its fiber profile.

Do not omit empty fibers

Listing only the values that occur in g's table gives 4↦{1,2} and 6↦{3} and misses the target 5. The fiber profile must run through the declared codomain, and the empty fiber of 5 is exactly the evidence that g is not surjective (S10).

• |A|=|B|=3, so g is bijective → reject — g(1)=g(2)=4 with 1≠2, so g is not injective; the fiber of 5 is empty, so g is not surjective.
• k:{1,2}→{4,5,6} with k(1)=4, k(2)=5 is injective, hence bijective → reject — The fiber of 6 is empty, so k is not surjective; moreover |{1,2}|=2≠3, so no bijection {1,2}→{4,5,6} exists at all.
• g is not bijective, so no bijection A→B exists → reject — Testing a given function and existence are different questions; f is a bijection A→B (S07, S13).
• There is no function between empty sets, so ∅→∅ has no bijection → reject — The empty function ε=∅ is the unique function ∅→∅; injectivity and surjectivity hold vacuously, so it is a bijection (S15).

Result and limitations

The fiber profile of f (in the order 4, 5, 6) is (1,1,1), so f is bijective; the fiber profile of g is (2,0,1), so g is neither injective (g(1)=g(2)) nor surjective (5 has no preimage), even though |A|=|B|=3. In general a total function is bijective exactly when every fiber has exactly one element (S05). Existence is a separate question: a bijection A→B exists (f), no bijection {1,2,3}→{4,5} exists (indeed no injection does), and ∅→∅ has exactly one, the empty bijection.

• The general fact that finite sets admit a bijection exactly when they have the same number of elements is taken from the prerequisite finite_counting_basics and not proved here; this guide answers A→B by the witness f and proves directly that there is no injection from a 3-element set to a 2-element set.
• The counting rule count_maps (27 and 6) is a prerequisite; S14 is illustrative and the main conclusions do not depend on it.

Verification and source binding

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

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

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