Commit 2022-01-10 01:23 99fe7acb

View on Github →

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.

Estimated changes

Modified src/data/set/function.lean

added theorem function.inv_fun_on_eq

added theorem function.inv_fun_on_mem

added theorem function.inv_fun_on_neg

added theorem function.inv_fun_on_pos

Modified src/logic/function/basic.lean

deleted theorem function.inv_fun_on_eq'

deleted theorem function.inv_fun_on_eq

deleted theorem function.inv_fun_on_mem

deleted theorem function.inv_fun_on_neg

deleted theorem function.inv_fun_on_pos

Modified src/measure_theory/covering/vitali.lean