Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.inv_fun_neg

Modification history

2021-11-29 17:49

src/logic/function/basic.lean

chore(logic/function): allow `Sort*` in `function.inv_fun` (#10526)

Modified function.inv_fun_neg View on Github →

2020-03-15 04:22

src/logic/function.lean

refactor(logic/function): inv_fun takes a nonempty instance instead of inhabited (#2148)

Modified function.inv_fun_neg View on Github →

2019-03-05 09:21

src/logic/function.lean

feat(logic/function): add inv_fun_neg

Added function.inv_fun_neg View on Github →