Inverse functions: exchanging a finite bijection table and inverting an affine map with nonzero slope

Goal and scope

(1) A={1,2,3}, B={4,5,6}, p(1)=5, p(2)=6, p(3)=4. First confirm that p is a bijection, then exchange its ordered pairs to get a candidate q, validate q as a total function B→A, and check q(p(x))=x and p(q(y))=y separately. (2) f:ℝ→ℝ, f(x)=−4x+6 (m=−4≠0): find the inverse g(y)=uy+v with u, v reduced rationals with positive denominators, and verify both identities for all reals. (3) Show that the exchanged table of h(1)=4, h(2)=4, h(3)=6 is not a function B→A, and that f^{-1} is not 1/f.

Follows the MKO assumptions: a finite table is first shown to be a bijection on the declared A→B (a1); a candidate is first validated as a total function and then both identities are checked (a2); the affine example is f:ℝ→ℝ with m≠0, coefficients as reduced rationals with positive denominators (a3). The affine part is proved for all reals by algebraic identities, not by sampling. General one-sided inverse theory, uniqueness of inverses and machine proofs are not treated; the canonical MKO and its English edition are not changed.

Givens and symbols

• function_def
• injective_surjective_def
• composition_def
• frac_rules
• distributive
• numeric_evaluation

• G1 — A={1,2,3}, B={4,5,6}; p:A→B with p(1)=5, p(2)=6, p(3)=4.
• G2 — f:ℝ→ℝ, f(x)=−4x+6, that is m=−4 and b=6.
• G3 — h:A→B with h(1)=4, h(2)=4, h(3)=6.
• G4 — Acceptance test (MKO a2): a candidate g is the inverse of a bijection f:A→B exactly when g is a total function B→A, g(f(x))=x for every x∈A, and f(g(y))=y for every y∈B.

• p,q — the finite bijection table and the exchanged table
• f,g — the affine map f(x)=−4x+6 and its inverse
• h — a non-bijective finite table
• R^{\mathsf T} — the exchanged relation {(b,a) ∣ (a,b)∈R}
• \mathrm{id}_A — the identity function on A

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.
• composition_def · prerequisite — Composition: for f:A→B and g:B→C, g∘f:A→C is defined by (g∘f)(a)=g(f(a)).
• frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
• 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.
• 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.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• eq_congruence · prerequisite — Congruence of equality: if u=v, applying the same defined operation f to both sides gives f(u)=f(v). Operating on one side only is not an instance of this rule.
• mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined.
• add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• add_zero · prerequisite — Additive identity: u+0=u.
• mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• mul_one · prerequisite — Multiplicative identity: 1·u=u.
• iff_intro · prerequisite — Biconditional: P⇔Q holds exactly when both P⇒Q and Q⇒P hold.
• neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv.
• 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.
• mko_inverse_def · cited — If f:A→B is bijective, its inverse g:B→A assigns each b its unique preimage and satisfies g(f(x))=x for x∈A and f(g(y))=y for y∈B. A finite bijection table can be inverted by exchanging ordered pairs. For nonbijective f, the exchanged table is not automatically an inverse on all of B. · mko-inverse-function
• mko_bijective_fiber · 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. · mko-bijective
• swap_table · prerequisite — Exchanged table: the exchange of a relation R⊆A×B is R^T={(b,a) ∣ (a,b)∈R}⊆B×A. The number of times b occurs as a first coordinate in R^T equals the number of times it occurs as a second coordinate in R.
• L_solve_affine · lemma — For reals m≠0, b, x, y: y=mx+b ⇔ x=(y−b)/m.

Main derivation

p(1)=5,\ p(2)=6,\ p(3)=4

p^{-1}(\{4\})=\{3\},\ p^{-1}(\{5\})=\{1\},\ p^{-1}(\{6\})=\{2\}\ \Rightarrow\ p\ \text{bijective}

p=\{(1,5),(2,6),(3,4)\}

q=p^{\mathsf T}=\{(5,1),(6,2),(4,3)\}

q=\{(4,3),(5,1),(6,2)\}

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

x\in A=\{1,2,3\}

q(p(x))=x\ \ \forall x\in A

y\in B=\{4,5,6\}

p(q(y))=y\ \ \forall y\in B

q:B\to A\ \text{total},\ q\circ p=\mathrm{id}_A,\ p\circ q=\mathrm{id}_B

q=p^{-1}

y=-4x+6

x=\frac{y-6}{-4}

\forall y\in\mathbb{R}:\ \bigl(f(x)=y\iff x=\tfrac{y-6}{-4}\bigr)

f^{-1}(\{y\})=\{\tfrac{y-6}{-4}\}\ \Rightarrow\ f\ \text{bijective}

y\in\mathbb{R}

g(y)=\frac{y-6}{-4}

\frac{y-6}{-4}

-\frac{1}{4}y+\frac{3}{2}

x\in\mathbb{R}\ \text{arbitrary}

g(f(x))=-\tfrac{1}{4}(-4x+6)+\tfrac{3}{2}=x

y\in\mathbb{R}\ \text{arbitrary}

f(g(y))=-4\bigl(-\tfrac{1}{4}y+\tfrac{3}{2}\bigr)+6=y

g\ \text{total},\ g\circ f=\mathrm{id}_{\mathbb{R}},\ f\circ g=\mathrm{id}_{\mathbb{R}}

f^{-1}(y)=-\tfrac{1}{4}y+\tfrac{3}{2}

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

f^{-1}\neq\frac{1}{f}

h^{\mathsf T}=\{(4,1),(4,2),(6,3)\}

h^{\mathsf T}\ \text{not a function}\ B\to A

\text{S06, S13, S14, S15}

q=p^{-1};\ f^{-1}(y)=-\tfrac{1}{4}y+\tfrac{3}{2};\ h^{\mathsf T}\ \text{rejected};\ f^{-1}\neq 1/f

Substeps and lemmas

y=mx+b

y-b=mx

y-b=mx

x=\frac{y-b}{m}

\frac{y-6}{-4}

\frac{y}{-4}-\frac{6}{-4}

\frac{y}{-4}-\frac{6}{-4}

-\frac{1}{4}y+\frac{3}{2}

Reverse audits

• S16 · sufficient_goal_reduction · S06, S13, S14, S15, and_intro_elim — Goal G is the three parts of the goal. The sufficient condition H is the conjunction of S06, S13, S14 and S15, each proved forwards from the givens; H⇒G uses only conjunction introduction.
• S15 · premise_audit · function_def, swap_table, G3 — Failure of either requirement suffices to refute 'is a function'; here both fail. The conclusion concerns h only and does not affect p or f.
• S14 · premise_audit · function_def, numeric_evaluation, S13 — Refuting equality of two functions needs only one input where they differ; the step does not claim they differ at every point.
• S13 · premise_audit · S09, S11, S12, mko_inverse_def — All three acceptance conditions hold one by one; the concrete instance is an illustration, not part of the proof.
• S12 · premise_audit · composition_def, distributive, neg_mul, forall_intro — Symmetric to S11; this side does not follow from S11 and is proved on its own.
• S11 · premise_audit · composition_def, distributive, neg_mul, forall_intro — It needs f(x)∈ℝ to lie in the domain of g so the composition is defined; the generalization to all x relies only on x being arbitrary.
• S10.2 · inverse_equivalence · frac_rules, neg_mul — Multiplying numerator and denominator by −1 and reducing are rewritings of equal values and can be undone.
• S10.1 · inverse_equivalence · frac_rules — The fraction addition rule holds both ways; its only condition is a nonzero denominator.
• S10 · inverse_equivalence · frac_rules, neg_mul — Both sub-steps S10.1 and S10.2 are identities valid for all y, so the two expressions define the same function.
• S09 · premise_audit · S08, mko_inverse_def, function_def — This only names the function by the unique preimage; both identities are still verified separately in S11 and S12.
• S08 · premise_audit · S07, mko_bijective_fiber, iff_intro — Both directions are used: ⇐ alone gives only surjectivity and ⇒ alone gives only injectivity.
• S07.2 · inverse_equivalence · mul_inverse_nonzero, eq_congruence — Multiplying by 1/m and by m undo each other, given m≠0, which is exactly the condition of MKO a3.
• S07.1 · inverse_equivalence · eq_congruence, add_inverse — Subtracting b and adding b undo each other and are possible for every real b.
• S07 · inverse_equivalence · L_solve_affine — Both directions of the lemma are proved in the sub-steps, and the condition −4≠0 holds.
• S06 · premise_audit · S03, S04, S05, mko_inverse_def — All three conditions are needed together; one identity alone is not enough (see the error controls).
• S05 · premise_audit · case_analysis, composition_def, S03 — The values of q lie in A, so p∘q is defined; the three cases exhaust B.
• S04 · premise_audit · case_analysis, composition_def, S03 — The composition is defined because the values of p lie in B, the domain of q; the three cases exhaust A. This is one identity only; the other side is S05.
• S03 · premise_audit · S01, swap_table, function_def — Totality needs every fiber to have at least one element (p surjective) and single-valuedness needs at most one (p injective); both come from S01. If p were not bijective this step would fail (see S15).
• S02 · premise_audit · swap_table, cartesian_product_def — This only constructs and names a set; it does not claim q is a function.
• S01 · premise_audit · G1, mko_bijective_fiber, set_builder — It needs all three inputs scanned and all three targets of the declared codomain checked; only the ⇐ direction of the fiber characterization is used.

Error controls and negative controls

The inverse is not the reciprocal

One misconception identified in the MKO is reading f^{-1} as 1/f. The superscript −1 means inverse under composition: f^{-1}(2)=1 but 1/f(2)=−1/2 (S14). Also 1/f is undefined at x=3/2 (f(3/2)=0), while f^{-1} is defined at every real.

Exchanging a non-bijective table does not give an inverse

The other misconception is to exchange a table whether or not it is bijective. h has fiber profile (2,0,1); after exchanging, 4 has two values and 5 has none, so it is not a function B→A (S15). The MKO requires establishing bijectivity first (a1) and only then exchanging.

Both identities must be checked

If only one side holds, the candidate is not an inverse. Example: p′:{1,2}→{4,5,6} with p′(1)=4, p′(2)=5; the candidate r:{4,5,6}→{1,2} with r(4)=1, r(5)=2, r(6)=1 is a total function and r(p′(x))=x for every x∈{1,2}, but p′(r(6))=p′(1)=4≠6. r is only a left inverse. This guide checks both sides for q and for g (S04, S05, S11, S12).

• g(y)=1/(−4y+6) is the inverse of f → reject — This is 1/f, not the inverse: f(0)=6, and 1/(−4·6+6)=−1/18≠0, so g(f(0))≠0.
• The exchanged table {(4,1),(4,2),(6,3)} of h is the inverse of h → reject — It is not a function B→A: 4 has two values and 5 has none; h is not bijective.
• r(4)=1, r(5)=2, r(6)=1 satisfies r(p′(x))=x, so r is the inverse of p′ → reject — The other side fails: p′(r(6))=p′(1)=4≠6.
• The inverse of f(x)=−4x+6 is g(y)=(y+6)/(−4) → reject — Sign error: f(0)=6, and (6+6)/(−4)=−3≠0; the correct inverse is (y−6)/(−4).

Result and limitations

p has fiber profile (1,1,1) and is bijective; the exchanged table q is a total function B→A with q(4)=3, q(5)=1, q(6)=2, and q∘p=id_A, p∘q=id_B, so q=p^{-1}. f(x)=−4x+6 is bijective with inverse f^{-1}(y)=(y−6)/(−4)=−(1/4)y+3/2, i.e. u=−1/4 and v=3/2, and both identities hold for all reals. The exchanged table of h is not a function B→A (4 has two values, 5 has none); f^{-1}(2)=1 while 1/f(2)=−1/2, so f^{-1}≠1/f.

• This guide does not separately prove that inverses are unique; it verifies only that the constructed q and g satisfy the MKO's two-sided definition.
• N3 to N5 are identity checks of degree-one polynomials on a grid, independent of the algebra in S10 to S12.

Verification and source binding

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

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

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