Commit 2022-06-20 11:25 320ea398
View on Github →feat(data/dfinsupp/basic): add missing lemmas about single
(#14815)
These lemmas were missed in #13076:
comap_domain_single
comap_domain'_single
sigma_curry_single
sigma_uncurry_single
extend_with_single_zero
extend_with_zero
These are useful since many induction principles replace a genericdfinsupp
withdfinsupp.single
.