Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-07-08 14:39 e5d5abd9

View on Github →

feat(data/pfun,...): add some isomorphism theorems

Estimated changes

Modified data/equiv/basic.lean

added def equiv.set_value

added theorem equiv.set_value_eq

Modified data/fintype.lean

Modified data/list/basic.lean

added theorem list.filter_of_map

Modified data/multiset.lean

added def multiset.strong_induction_on

deleted theorem multiset.strong_induction_on

Modified data/pfun.lean

added def pfun.equiv_subtype

added theorem roption.eta

added theorem roption.of_option_dom

added theorem roption.of_option_eq_get