Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.inv_fun_comp

Modification history

2017-11-09 12:33
logic/function.lean
feat(data/set/finite): finite_of_finite_image
Added function.inv_fun_compView on Github →