Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.inv_fun_on_neg

Modification history

2022-01-10 01:23

src/data/set/function.lean

chore(data/set/function): move inv_fun_on out of `logic/function/basic` (#11330) …

Modified function.inv_fun_on_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_on_neg View on Github →

2017-10-15 01:58

logic/function.lean

feat(*): working on list/basic, robusting simp proofs

Added function.inv_fun_on_neg View on Github →