basic` (#11330)

Commit

4 years ago

chore(data/set/function): move inv_fun_on out of `logic/function/basic` (#11330) This removes `function.inv_fun_on_eq'` as it is a duplicate of `inj_on.left_inv_on_inv_fun_on`.

Author

eric-wieser

Parents

6a109397

mathlib3 99fe7acb - chore(data/set/function): move inv_fun_on out of `logic/function/basic` (#11330)

mathlib3
99fe7acb - chore(data/set/function): move inv_fun_on out of `logic/function/basic` (#11330)