Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-04 18:03 bbf97744

View on Github →

feat(data/fintype/basic): inv of inj on deceq (#5872)

Estimated changes

Modified src/data/fintype/basic.lean

added theorem function.embedding.inv_fun_restrict

added def function.embedding.inv_of_mem_range

added theorem function.embedding.inv_of_mem_range_surjective

added theorem function.embedding.left_inv_of_inv_of_mem_range

added theorem function.embedding.right_inv_of_inv_of_mem_range

added theorem function.injective.inv_fun_restrict

added def function.injective.inv_of_mem_range

added theorem function.injective.inv_of_mem_range_surjective

added theorem function.injective.left_inv_of_inv_of_mem_range

added theorem function.injective.right_inv_of_inv_of_mem_range

Modified src/data/set/basic.lean

added theorem function.injective.exists_unique_of_mem_range

added theorem function.injective.mem_range_iff_exists_unique

Modified src/logic/function/basic.lean