Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-11 16:44 3a88a9ea

View on Github →

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

Estimated changes

Modified src/data/subtype.lean

added theorem subtype.coind_bijective

added theorem subtype.coind_surjective

added theorem subtype.map_involutive