Lemma·L03
The inverse of a bijection
A bijection can be undone: its converse is a bijection the other way.
In words
If f is a bijection from A to B, then reading it backwards gives a bijection from B to A: it undoes f, and is undone by f.
Never needed: F03 · F04 · F05 · F06 · F08 · F10 · F11 · F12 · F13 · A01 · A02 · A03 · A04 · A05 · A06 · A07 · A08 (computed from the citation graph, not asserted).
Proof
- 1is a function : let . By surjectivity of there is with , so by D019: has at least one value. If and , then , so by injectivity: at most one value. Hence exactly one, and by D013.
- 2The two cancellation identities: for , the pair lies in , and since is a function, . For , is by construction some with , so .
- 3is injective: if , apply to both sides; step 2 gives (substitutivity).
- 4is surjective onto : given , take ; then by step 2. Hence is an injective surjection , a bijection.
∎
Remarks
This is the symmetry of the "same size" relation: if
matches perfectly with
, then
matches perfectly with
(L22 uses exactly this). The notation
for the inverse function agrees with the converse-relation notation because the inverse function is the converse relation, merely observed to be a function when
is a bijection.