Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.inv_fun_on_pos

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_pos View on Github →

2017-10-15 01:58

logic/function.lean

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

Added function.inv_fun_on_pos View on Github →