TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-08-06 (claude-opus-5)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

$f : A \to B$ is a bijection if and only if there is a function $g : B \to A$ with $g \circ f = Δ_{A}$ and $f \circ g = Δ_{B}$ ; such a $g$ is unique, equals the inverse relation $f^{- 1}$ , and is itself a bijection

Statement

Let $f : A \to B$ . Then $f$ is a bijection if and only if there is a function $g : B \to A$ with $g \circ f = Δ_{A}$ and $f \circ g = Δ_{B}$ . When such a $g$ exists it is unique, it is the inverse relation $f^{- 1}$ , and it is itself a bijection $B \to A$ .

No choice principle is used: the value $g (b)$ is the unique $a$ with $f (a) = b$ , so it is determined rather than selected.

Facts & Assumptions

Given: a function $f : A \to B$ .

[L1]

$f$ is injective (one-to-one) if $f (x) = f (y)$ implies $x = y$ , for all $x, y \in A$ (Injection, surjection, bijection).

[L2]

$f$ is surjective (onto) if for every $b \in B$ there is some $x \in A$ with $f (x) = b$ (Injection, surjection, bijection).

[L3]

We write $f : A \to B$ , and say $f$ is a function from $A$ to $B$ , when $f$ is a function with $dom f = A$ and $ran f \subseteq B$ (A function is a relation $f$ with $(a, b) \in f$ and $(a, c) \in f$ implying $b = c$ ; $f : A \to B$ , the value $f (a)$ , domain and codomain).

[L4]

$(b, a) \in R^{- 1}$ holds if and only if $(a, b) \in R$ (The inverse relation $R^{- 1}$ , the composite $S \circ R$ , and the restriction $R ↾ A$ ).

[L5]

$dom (R^{- 1}) = ran R$ and $ran (R^{- 1}) = dom R$ ( $T \circ (S \circ R) = (T \circ S) \circ R$ , $(S \circ R)^{- 1} = R^{- 1} \circ S^{- 1}$ , $(R^{- 1})^{- 1} = R$ , $dom (R^{- 1}) = ran R$ , and $Δ_{B} \circ R = R = R \circ Δ_{A}$ for a relation $R$ from $A$ to $B$ ).

[L6]

$g \circ f$ is a function, $dom (g \circ f) = f^{- 1} [dom g]$ , and $(g \circ f) (x) = g (f (x))$ for every $x$ in that domain (If $f$ and $g$ are functions then $g \circ f$ is a function with domain $f^{- 1} [dom g]$ and $(g \circ f) (x) = g (f (x))$ there; $Δ_{A}$ is a function with $Δ_{A} (a) = a$ ; and $f \circ Δ_{A} = f = Δ_{B} \circ f$ for $f : A \to B$ ).

[L7]

$Δ_{A}$ is a function with $dom Δ_{A} = A$ and $Δ_{A} (a) = a$ for every $a \in A$ (If $f$ and $g$ are functions then $g \circ f$ is a function with domain $f^{- 1} [dom g]$ and $(g \circ f) (x) = g (f (x))$ there; $Δ_{A}$ is a function with $Δ_{A} (a) = a$ ; and $f \circ Δ_{A} = f = Δ_{B} \circ f$ for $f : A \to B$ ).

[L8]

$f = g$ if and only if $dom f = dom g$ and $f (x) = g (x)$ for every $x \in dom f$ (Functions $f$ and $g$ are equal if and only if $dom f = dom g$ and $f (x) = g (x)$ for every $x$ in that common domain).

[L9]

$ran R : = {b : \exists a (a, b) \in R}$ (Relation, $dom R$ , $ran R$ , $fld R$ , and the specialisations "relation from $A$ to $B$ " and "relation on $A$ ").

[L10]

$(a, b) \in Δ_{A}$ holds if and only if $a = b$ and $a \in A$ (The identity relation $Δ_{A} = {(a, b) \in A \times A : a = b}$ and the membership relation $\in_{A} = {(a, b) \in A \times A : a \in b}$ ).

Proof

technique · direct

1.1L1L2L3L4L5L9

Suppose $f$ is a bijection. The inverse relation $f^{- 1}$ is a function: if $(b, a)$ and $(b, a^{'})$ lie in it then $f (a) = b = f (a^{'})$ , so $a = a^{'}$ by injectivity. Its domain is $ran f$ , which is $B$ by surjectivity, and its range is $dom f = A$ ; hence $f^{- 1} : B \to A$ .

1.2L1L2L6L7L10

Conversely, suppose $g : B \to A$ satisfies $g \circ f = Δ_{A}$ and $f \circ g = Δ_{B}$ . If $f (a) = f (a^{'})$ then $a = g (f (a)) = g (f (a^{'})) = a^{'}$ , so $f$ is injective; and any $b \in B$ satisfies $b = Δ_{B} (b) = f (g (b))$ , so $b$ is a value of $f$ and $f$ is surjective. Hence $f$ is a bijection.

1.3L6L7L8

Any two such functions agree: if $g$ and $g^{'}$ both satisfy the two identities then, for $b \in B$ , $f (g^{'} (b)) = b$ , so $g (b) = g (f (g^{'} (b))) = Δ_{A} (g^{'} (b)) = g^{'} (b)$ ; both have domain $B$ , so $g = g^{'}$ .

2.1L4L6L7L8step 1.1

For a bijection $f$ , the function $f^{- 1}$ of step 1.1 satisfies the two identities: $f^{- 1} \circ f$ and $Δ_{A}$ are functions with domain $A$ , and $f^{- 1} (f (a)) = a = Δ_{A} (a)$ for $a \in A$ ; likewise $f \circ f^{- 1}$ and $Δ_{B}$ are functions with domain $B$ agreeing at every point.

2.2step 1.2

Such a $g$ is itself a bijection: $f$ is a function $A \to B$ with $f \circ g = Δ_{B}$ and $g \circ f = Δ_{A}$ , which is the hypothesis of step 1.2 applied to $g$ in place of $f$ .

3.1step 1.3step 2.1

Such a $g$ is the inverse relation: $f^{- 1}$ satisfies the two identities by step 2.1, and step 1.3 says there is only one function that does.

4.1step 1.1step 1.2step 1.3step 2.1step 2.2step 3.1∎

The two directions, the uniqueness, the identification with $f^{- 1}$ and the bijectivity of $g$ are established, which is the statement.

$f : A \to B$ is a bijection if and only if there is a function $g : B \to A$ with $g \circ f = Δ_{A}$ and $f \circ g = Δ_{B}$ ; such a $g$ is unique, equals the inverse relation $f^{- 1}$ , and is itself a bijection

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

f:A→Bf:A→B is a bijection if and only if there is a function g:B→Ag:B→A with g∘f=ΔAg∘f=ΔA​ and f∘g=ΔBf∘g=ΔB​; such a gg is unique, equals the inverse relation f−1f−1, and is itself a bijection

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

$f : A \to B$ is a bijection if and only if there is a function $g : B \to A$ with $g \circ f = Δ_{A}$ and $f \circ g = Δ_{B}$ ; such a $g$ is unique, equals the inverse relation $f^{- 1}$ , and is itself a bijection