## Stream: maths

### Topic: bijection negation

#### Sean Leather (May 17 2018 at 12:21):

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

#### Chris Hughes (May 17 2018 at 12:23):

It doesn't need to be bijective.

#### Sean Leather (May 17 2018 at 12:26):

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 (May 17 2018 at 12:27):

Or perhaps something simpler.

#### Mario Carneiro (May 17 2018 at 12:28):

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

#### Kevin Buzzard (May 17 2018 at 12:28):

This is just a rw.

#### Sean Leather (May 17 2018 at 12:30):

Ah, right. Silly me!

Last updated: May 18 2021 at 07:19 UTC