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.
Injection, surjection, bijection
Definition
Let and be sets and let be a function (A function is a relation with and implying ; , the value , domain and codomain).
- is injective (one-to-one) if implies , for all .
- is surjective (onto) if for every there is some with ; equivalently, the image equals .
- is bijective if it is both injective and surjective.
For we write for the image of , and for we write for the preimage of ; these are the image and preimage of a set under read as a relation (The image and the preimage of a set under a relation).
Remarks
-
Composition. If and are both injective then so is , since forces and then ; if both are surjective then so is , since any is for some and that is for some . Hence a composition of bijections is a bijection. These verifications, together with the two partial converses, are For and : if both are injective so is ; if both are surjective so is ; if is injective so is ; and if is surjective so is .
-
Inverses. is bijective exactly when there is a function with for all and for all ; that two-sided inverse is unique, and it is itself a bijection. Injectivity alone gives a bijection from onto the image , and hence an inverse defined on only. No choice principle is involved: the value is the unique with , so it is determined rather than selected. The full statement, with the uniqueness of the two-sided inverse, is is a bijection if and only if there is a function with and ; such a is unique, equals the inverse relation , and is itself a bijection; the corresponding statement for an arbitrary surjection is not available at this point in the reading order, because a right inverse for every surjection is equivalent to the Axiom of Choice.
-
What this item does and does not do. A function is a set of ordered pairs, single valued and total on (A function is a relation with and implying ; , the value , domain and codomain); ordered pairs, Cartesian products, images and preimages are fixed by The Kuratowski ordered pair , The Cartesian product and The image and the preimage of a set under a relation. This item only fixes the three adjectives and the notation used for them. Nothing here is proved.