Commit 2020-10-16 00:56 dca1393e
View on Github →feat(data/equiv/basic): add equiv.set.compl (#4630)
Given an equivalence between two sets e₀ : s ≃ t, the set of
e : α ≃ β that agree with e₀ on s is equivalent to sᶜ ≃ tᶜ.
Also add a bunch of lemmas to data/set/function; some of them are
used in the definition of equiv.set.compl.