Definition inj_equi

Definition. inj_equi
inj f X Y ↔ map f X Y ∧ ∀a. ∀b. a ∈ X → b ∈ X → app f a = app f b → a = b

A mapping f from X to Y is called injective if any two elements of X with the same image must be equal.