Zulip Chat Archive

Stream: maths

Topic: bijection negation


view this post on Zulip 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?

view this post on Zulip Chris Hughes (May 17 2018 at 12:23):

It doesn't need to be bijective.

view this post on Zulip 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?

view this post on Zulip Sean Leather (May 17 2018 at 12:27):

Or perhaps something simpler.

view this post on Zulip Mario Carneiro (May 17 2018 at 12:28):

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

view this post on Zulip Kevin Buzzard (May 17 2018 at 12:28):

This is just a rw.

view this post on Zulip Sean Leather (May 17 2018 at 12:30):

Ah, right. Silly me!


Last updated: May 18 2021 at 07:19 UTC