Defsurj
Establish a surjective mapping between two domains.
This is a specialization of defmapping where
the :alpha-of-beta-thm input is t.
See the documentation of defmapping.
Here `surjective' refers to the \alpha conversion.
Its right inverse conversion \beta is injective.
Subtopics
- Defsurj-implementation
- Implementation of defsurj.
