bijection negation

Stream: maths

[Sean Leather]

Is there a property like ∀ ⦃a₁ a₂⦄, f a₁ ≠ f a₂ → a₁ ≠ a₂ for a bijective f?

[Chris Hughes]

It doesn't need to be bijective.

[Sean Leather]

True. So, I have a function that already needs to be an injection. Would be it be preferable to use the above property directly, or, if it I make a bijection, can I derive that property?

[Sean Leather]

Or perhaps something simpler.

[Mario Carneiro]

That theorem is true for any function whatsoever. It is mt (congr_arg f)

[Kevin Buzzard]

This is just a rw.

[Sean Leather]

Ah, right. Silly me!