Commit 2025-03-20 11:09 88f302b1
View on Github →feat: corestrict an equivalence to a finset (#22534)
Given an equivalence e : α ≃ β and s : Finset β, restrict e to an equivalence from e ⁻¹' s to s.
feat: corestrict an equivalence to a finset (#22534)
Given an equivalence e : α ≃ β and s : Finset β, restrict e to an equivalence from e ⁻¹' s to s.