Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-09 10:43 4fc67f8f

View on Github →

feat(data/fintype): add choose_unique and construct inverses to bijections (#421)

Estimated changes

Modified data/finset.lean

added def finset.choose

added theorem finset.choose_mem

added theorem finset.choose_property

added theorem finset.choose_spec

added def finset.choose_x

Modified data/fintype.lean

added def fintype.bij_inv

added theorem fintype.bijective_bij_inv

added def fintype.choose

added theorem fintype.choose_spec

added def fintype.choose_x

added theorem fintype.left_inverse_bij_inv

added theorem fintype.right_inverse_bij_inv

Modified data/list/basic.lean

added def list.choose

added theorem list.choose_mem

added theorem list.choose_property

added theorem list.choose_spec

added def list.choose_x

Modified data/multiset.lean

added def multiset.choose

added theorem multiset.choose_mem

added theorem multiset.choose_property

added theorem multiset.choose_spec

added def multiset.choose_x