Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorroglo
    • CommentTimeSep 4th 2019
    In the page "injection", it says "strongly injective if f(x)≠f(y) whenever x≠y (which implies that the function is injective)". I would say the other way around: "injective" implies this "strongly injective" definition. So "strongly injective" should be renamed "weakly injective". Am I wrong?
    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeSep 4th 2019

    The two statements are equivalent in classical mathematics. In constructive mathematics, the statement “f(x)f(y)f(x)\neq f(y) whenever xyx\neq y” is weaker than injectivity if \neq refers to the denial inequality, but stronger than injectivity if \neq refers to a tight apartness relation. So the page is correct as written, since it mentions tight apartness; but it could stand to be expanded and clarified.

    • CommentRowNumber3.
    • CommentAuthorroglo
    • CommentTimeSep 5th 2019
    • (edited Sep 5th 2019)
    .