Mathlib v3 is deprecated. Go to Mathlib v4

Theorem equiv.of_preimage_equiv_map

Modification history

2022-05-04 20:04

src/logic/equiv/set.lean

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

Added equiv.of_preimage_equiv_map View on Github →