Commit 2025-11-07 22:59 e8ebb321
View on Github →feat(Subtype): SurjOn versions of coind_surjective and coind_bijective (#31349)
Conditions of theorems Subtype.coind_surjective and Subtype.coind_bijective imply that the subtype coincides with the whole type, which makes these theorems not very useful. This PR deprecates them and proves Set.SurjOn versions.