Joint injectivity of a pair of functions

ID: joint-injectivity-of-a-pair-of-functions

The pairing map to a Cartesian product is injective exactly when its coordinate functions are jointly injective in the displayed sense. Either coordinate being injective is sufficient, but neither need be injective individually. For example, pairing three points with distinguishes all points even though each coordinate separately identifies two of them.

New to topics? Read the docs here!