Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subtype.coind_surjective

Modification history

2021-09-03 20:53

src/data/subtype.lean

docs(data/subtype): add module docstring (#8900)

Modified subtype.coind_surjective View on Github →

2020-12-11 16:44

src/data/subtype.lean

chore(data/subtype): Add coind_bijective and map_involutive (#5319)

Added subtype.coind_surjective View on Github →