Commit 2022-10-03 08:59 3cf2547c

feat(data/fintype/basic): Existence of a bijection with specified behaviour on a subset (#16479) Given a function f : α → β which is injective on a set s in α, and a set t in β which has the same finite cardinality as the type α and which contains the image f '' s, extend/modify to a bijection between α and t which agrees on s with the original f.