Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-05-09 06:04 b31c30db

View on Github →

refactor(logic/function): constructive proof of cantor_injective

Estimated changes

modified theorem function.cantor_injective