Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-28 17:00 0d6548fc

View on Github →

chore(*): a few lemmas about `range_splitting (#10016)

Estimated changes

Modified src/data/equiv/set.lean

added theorem equiv.coe_of_injective_symm

Modified src/data/set/basic.lean

added theorem set.coe_comp_range_factorization

added theorem set.preimage_range_splitting

added theorem set.right_inverse_range_splitting

Modified src/logic/function/basic.lean

added theorem function.left_inverse.right_inverse_of_injective

added theorem function.left_inverse.right_inverse_of_surjective