# Inverse functions: exchanging a finite bijection table and inverting an affine map with nonzero slope [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-inverse-function/) 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-inverse-function-01 · production-20261019-adopted-96 ## 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 S01 · impliesBefore p(1)=5,\ p(2)=6,\ p(3)=4 After p^{-1}(\{4\})=\{3\},\ p^{-1}(\{5\})=\{1\},\ p^{-1}(\{6\})=\{2\}\ \Rightarrow\ p\ \text{bijective} Conditions: none Rule: mko_bijective_fiber · Uses: G1, mko_bijective_fiber Leaf basis: mko_bijective_fiber + set_builder + numeric_evaluation MKO assumption a1 requires first establishing that p is a bijection on the declared A→B. Scanning the three elements of A: target 4 is reached only from 3, 5 only from 1, and 6 only from 2. Every target of B has a fiber with exactly one element, so p is bijective. S02 · definitionBefore p=\{(1,5),(2,6),(3,4)\} After q=p^{\mathsf T}=\{(5,1),(6,2),(4,3)\} Conditions: none Rule: swap_table · Uses: G1 Leaf basis: swap_table + cartesian_product_def Write p as a set of ordered pairs and exchange the two coordinates of each pair to get the candidate q. At this point q is only a subset (a relation) of B×A; whether it is a function B→A has to be checked separately (a2). S03 · impliesBefore q=\{(4,3),(5,1),(6,2)\} After q:B\to A\ \text{total};\ q(4)=3,\ q(5)=1,\ q(6)=2 Conditions: none Rule: function_def · Uses: S01, S02 Leaf basis: function_def + swap_table + set_builder By swap_table, the number of times b occurs as a first coordinate in q equals the number of times b occurs as a value of p, which is the size of the fiber p^{-1}({b}), equal to 1 by S01. So 4, 5, 6 each occur exactly once: every b has a value (total) and only one (single-valued), and the values 3, 1, 2 lie in A. q is a total function B→A. S04 · impliesBefore x\in A=\{1,2,3\} After q(p(x))=x\ \ \forall x\in A Conditions: none Rule: case_analysis · Uses: G1, S03 Leaf basis: case_analysis + composition_def + numeric_evaluation A has exactly three elements, so checking each one is a proof by exhaustive cases, not a sample: q(p(1))=q(5)=1, q(p(2))=q(6)=2, q(p(3))=q(4)=3. So q∘p=id_A. S05 · impliesBefore y\in B=\{4,5,6\} After p(q(y))=y\ \ \forall y\in B Conditions: none Rule: case_analysis · Uses: G1, S03 Leaf basis: case_analysis + composition_def + numeric_evaluation The second identity has to be checked separately, since the representative formula g(f(x))=x shows only one side: p(q(4))=p(3)=4, p(q(5))=p(1)=5, p(q(6))=p(2)=6. All three elements of B were checked, so p∘q=id_B. S06 · impliesBefore q:B\to A\ \text{total},\ q\circ p=\mathrm{id}_A,\ p\circ q=\mathrm{id}_B After q=p^{-1} Conditions: none Rule: mko_inverse_def · Uses: S03, S04, S05, G4 Leaf basis: mko_inverse_def + and_intro_elim All three requirements of G4 hold: q is a total function (S03), q∘p=id_A (S04) and p∘q=id_B (S05). Moreover q(b) is exactly the unique preimage of b found in S01, matching the MKO's definition. So q is the inverse of p. S07 · equivalentBefore y=-4x+6 After x=\frac{y-6}{-4} Conditions: -4\neq 0 Rule: L_solve_affine · Uses: G2 Leaf basis: eq_congruence + mul_inverse_nonzero Turn to the affine example. For any real y, by Lemma L_solve_affine (m=−4, b=6): y=−4x+6 ⇔ x=(y−6)/(−4). The lemma is proved in S07.1 and S07.2 and needs m=−4≠0. S08 · impliesBefore \forall y\in\mathbb{R}:\ \bigl(f(x)=y\iff x=\tfrac{y-6}{-4}\bigr) After f^{-1}(\{y\})=\{\tfrac{y-6}{-4}\}\ \Rightarrow\ f\ \text{bijective} Conditions: none Rule: mko_bijective_fiber · Uses: S07, mko_bijective_fiber Leaf basis: mko_bijective_fiber + set_builder + iff_intro For every real y: the ⇐ direction of S07 shows that the real number (y−6)/(−4) lies in the fiber of y (existence), and the ⇒ direction shows that every element of the fiber equals it (uniqueness). So every fiber has exactly one element and f is bijective, meeting the precondition of a1. S09 · definitionBefore y\in\mathbb{R} After g(y)=\frac{y-6}{-4} Conditions: none Rule: mko_inverse_def · Uses: S08 Leaf basis: mko_inverse_def + function_def By the MKO, the inverse sends each y to its unique preimage; by S08 that preimage is (y−6)/(−4). The denominator −4≠0, so it is defined for every real y and g is a total function ℝ→ℝ. S10 · equivalentBefore \frac{y-6}{-4} After -\frac{1}{4}y+\frac{3}{2} Conditions: -4\neq 0 Rule: frac_rules · Uses: S09 Leaf basis: frac_rules + neg_mul Rewrite in the form g(y)=uy+v to get u=−1/4 and v=3/2; details are in S10.1 and S10.2. This agrees with the MKO formula: u=1/m=1/(−4)=−1/4 and v=−b/m=−6/(−4)=3/2. Both coefficients are reduced, with positive denominators 4 and 2. S11 · impliesBefore x\in\mathbb{R}\ \text{arbitrary} After g(f(x))=-\tfrac{1}{4}(-4x+6)+\tfrac{3}{2}=x Conditions: none Rule: forall_intro · Uses: G2, S10 Leaf basis: composition_def + distributive + neg_mul + add_inverse + forall_intro Take any real x: g(f(x))=−(1/4)(−4x+6)+3/2=x−3/2+3/2=x (distributivity and sign rules). No extra condition was placed on x, so this holds for all reals; it is an algebraic identity, not a finite check. S12 · impliesBefore y\in\mathbb{R}\ \text{arbitrary} After f(g(y))=-4\bigl(-\tfrac{1}{4}y+\tfrac{3}{2}\bigr)+6=y Conditions: none Rule: forall_intro · Uses: G2, S10 Leaf basis: composition_def + distributive + neg_mul + add_inverse + forall_intro The other side: for any real y, f(g(y))=−4(−(1/4)y+3/2)+6=y−6+6=y. Both identities hold for all reals. S13 · impliesBefore g\ \text{total},\ g\circ f=\mathrm{id}_{\mathbb{R}},\ f\circ g=\mathrm{id}_{\mathbb{R}} After f^{-1}(y)=-\tfrac{1}{4}y+\tfrac{3}{2} Conditions: none Rule: mko_inverse_def · Uses: S09, S11, S12, G4 Leaf basis: mko_inverse_def + and_intro_elim + numeric_evaluation g is a total function (S09) and both identities hold (S11, S12), so by G4 g is the inverse of f. Concrete instance: f(2)=−2, and g(−2)=1/2+3/2=2, returning to 2. S14 · impliesBefore f^{-1}(2)=1,\ \frac{1}{f(2)}=-\frac{1}{2} After f^{-1}\neq\frac{1}{f} Conditions: none Rule: function_def · Uses: S13, G2 Leaf basis: function_def + numeric_evaluation + frac_rules f^{-1}(2)=−(1/4)·2+3/2=1, but f(2)=−2, so 1/f(2)=−1/2. The two functions take different values at the same input 2, so by the definition of equality of functions f^{-1}≠1/f. Moreover f(3/2)=0, so 1/f is not even defined at x=3/2, while f^{-1} is defined at every real. The superscript −1 means inverse under composition, not reciprocal. S15 · impliesBefore h^{\mathsf T}=\{(4,1),(4,2),(6,3)\} After h^{\mathsf T}\ \text{not a function}\ B\to A Conditions: none Rule: function_def · Uses: G3 Leaf basis: function_def + swap_table + set_builder Exchange the table of h: 4 is paired with both 1 and 2 (not single-valued) and 5 with nothing (not total), so both requirements of a function fail. This matches the fiber profile (2,0,1) of h: h is not bijective, and by a1 its exchanged table cannot serve as an inverse. In fact no r:B→A can satisfy h(r(y))=y for every y∈B, since y=5 would need h(r(5))=5, and 5 is not a value of h. S16 · impliesBefore \text{S06, S13, S14, S15} After q=p^{-1};\ f^{-1}(y)=-\tfrac{1}{4}y+\tfrac{3}{2};\ h^{\mathsf T}\ \text{rejected};\ f^{-1}\neq 1/f Conditions: none Rule: and_intro_elim · Uses: S06, S13, S14, S15 Leaf basis: and_intro_elim Collect the three parts: exchanging the finite bijection table gives the inverse q of p; the affine inverse has coefficients u=−1/4 and v=3/2; the exchanged table of the non-bijective h is rejected, and the inverse is distinguished from the reciprocal. ## Substeps and lemmas S07.1 · equivalentBefore y=mx+b After y-b=mx Conditions: none Rule: eq_congruence · Uses: eq_congruence Leaf basis: eq_congruence + add_assoc + add_comm + add_inverse + add_zero Subtract b from both sides: (mx+b)−b=mx (associativity and inverses for addition). The backward move is to add b to both sides. S07.2 · equivalentBefore y-b=mx After x=\frac{y-b}{m} Conditions: m\neq 0 Rule: mul_inverse_nonzero · Uses: S07.1, mul_inverse_nonzero Leaf basis: eq_congruence + mul_inverse_nonzero + mul_assoc + mul_comm + mul_one Since m≠0, 1/m exists; multiplying both sides by 1/m gives (y−b)/m=x. The backward move is to multiply both sides by m. If m=0 the step cannot be taken, and then f(x)=b is constant and not a bijection at all. S07.1 and S07.2 together prove Lemma L_solve_affine. S10.1 · equivalentBefore \frac{y-6}{-4} After \frac{y}{-4}-\frac{6}{-4} Conditions: -4\neq 0 Rule: frac_rules · Uses: S09, frac_rules Leaf basis: frac_rules Fractions with a common denominator: (a−c)/d=a/d−c/d with d=−4≠0. The backward move combines the two fractions again. S10.2 · equivalentBefore \frac{y}{-4}-\frac{6}{-4} After -\frac{1}{4}y+\frac{3}{2} Conditions: none Rule: frac_rules · Uses: S10.1, neg_mul Leaf basis: frac_rules + neg_mul + numeric_evaluation Move the negative denominator to the numerator: y/(−4)=−y/4=(−1/4)y; 6/(−4)=−6/4=−3/2 (reduced by gcd(6,4)=2), and subtracting −3/2 means adding 3/2. So u=−1/4 and v=3/2, with gcd(1,4)=1, gcd(3,2)=1 and positive denominators. ## 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 reciprocalOne 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 inverseThe 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 checkedIf 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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-inverse-function-01.json)