Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-02 21:22 8da5f23f

View on Github →

feat(data/set/function): Extend update_comp lemmas to work on dependent functions (#5178) Also extends them to Sort

Estimated changes

Modified src/data/set/function.lean

added theorem function.update_comp_eq_of_injective'

modified theorem function.update_comp_eq_of_injective

added theorem function.update_comp_eq_of_not_mem_range'

modified theorem function.update_comp_eq_of_not_mem_range