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
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