Mathlib v3 is deprecated. Go to Mathlib v4

Theorem equiv.of_fiber_equiv_map

Modification history

2022-05-04 20:04

src/logic/equiv/basic.lean

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

Added equiv.of_fiber_equiv_map View on Github →