# Surjectivity and codomain coverage

This English edition is an AI candidate and does not yet have an OCME Atlas (GPT-6) Twin closure receipt.

Surjectivity requires a permitted preimage for every codomain element; an output may have several preimages.

mko-surjective · definition · v0.10.0



## Mathematical statement

A total function f:A→B is surjective exactly when, for every b∈B, there exists x∈A with f(x)=b; equivalently, the attained range f[A] equals the declared codomain B. Surjectivity does not require a unique preimage.





## Representative formula (exact TeX)

f:A\to B





## Assumptions


- The domain, codomain, and total function are explicit.
- A replacement codomain must contain every existing output for the same table to remain a valid total function.





## Symbol scope


- f — specified total function
- A — domain
- B — declared codomain





## Intuition, definition, and misconceptions

For a finite table, the uncovered targets form B∖f[A]. Missing any target defeats surjectivity, while several inputs reaching one target do not.

For a specified t∈B, enumerate its preimages. The first preimage here means the numerically least input in the finite integer data; report none if the fiber is empty.

Changing the codomain from B to B2 may change surjectivity of the same output table. First check f[A]⊆B2, then ask whether f[A]=B2. Do not guess the codomain or discard attained outputs. The empty function ∅→∅ is surjective, while ∅→nonempty B is not.

Common errors include automatically identifying range with codomain, or using multiple preimages as an objection to surjectivity.





## Adopted derivation guide

[Surjectivity and codomain coverage: range, preimages and changing the codomain](https://ocme.evemisslab.com/en/derivations/derivation-mko-surjective-01/)The original MKO is retained. The guide has its own append-only revision and verification boundaries, not a new Lean proof.





## Prerequisites


- [Function mapping](https://ocme.evemisslab.com/en/mko/mko-function-mapping/) — Codomain and output eligibility are part of a function declaration.
- [Quantifiers and explicit domains](https://ocme.evemisslab.com/en/mko/mko-quantifier/) — Surjectivity requires a permitted preimage for every codomain element.





## Verification boundary

Finite codomain coverage can be recomputed completely; general surjectivity and preimage-selection formal obligations remain open.

not_formalized

This does not mean the content is false; it means no replayable computational or formal evidence is registered yet.





## Next obligation

Bind Function.Surjective, range, and legality of codomain changes.





## Same-source structured data

This page and the interactive view use the same object and existing language edition; this adds no proof or human review.

[Canonical MKO JSON](https://ocme.evemisslab.com/data/mko/surjective.json) · [Plain Markdown](https://ocme.evemisslab.com/en/mko/mko-surjective/index.md)