Skip to content

Generalize fsfun_injective_inP to arbitrary functions.#133

Merged
CohenCyril merged 1 commit intomath-comp:masterfrom
arthuraa:gen-fsfun_injective_inP
May 12, 2025
Merged

Generalize fsfun_injective_inP to arbitrary functions.#133
CohenCyril merged 1 commit intomath-comp:masterfrom
arthuraa:gen-fsfun_injective_inP

Conversation

@arthuraa
Copy link
Copy Markdown
Contributor

No description provided.

@arthuraa
Copy link
Copy Markdown
Contributor Author

Incidentally, we don't even need fsfun_injective_inP in this file anymore.

We could also prove the more restricted version from fset_injective_inP if we had an extensionality lemma eq_injectiveb (which is currently lacking in math-comp).

@CohenCyril CohenCyril merged commit f76b75a into math-comp:master May 12, 2025
17 of 20 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants