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