Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-10 20:33 7e06124c

View on Github →

feat(logic): add small theory on inverse functions

Estimated changes

Created logic/function_inverse.lean

added theorem set.has_left_inverse

added theorem set.has_right_inverse

added theorem set.injective_surj_inv

added def set.inv_fun

added theorem set.inv_fun_eq

added theorem set.inv_fun_eq_of_injective_of_right_inverse

added def set.inv_fun_on

added theorem set.inv_fun_on_eq

added theorem set.inv_fun_on_mem

added theorem set.inv_fun_on_neg

added theorem set.inv_fun_on_pos

added theorem set.left_inverse_inv_fun

added theorem set.right_inverse_inv_fun

added theorem set.right_inverse_surj_inv

added def set.surj_inv

added theorem set.surj_inv_eq