set): equivalences between all preimages gives an equivalence of domains (#13853)

Commit

3 years ago

feat(logic/equiv/set): equivalences between all preimages gives an equivalence of domains (#13853) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author

kim-em

Parents

edf6cefa

mathlib a80e5683 - feat(logic/equiv/set): equivalences between all preimages gives an equivalence of domains (#13853)

mathlib
a80e5683 - feat(logic/equiv/set): equivalences between all preimages gives an equivalence of domains (#13853)