Mathlib v3 is deprecated. Go to Mathlib v4

Theorem set.preimage_injective

Modification history

2023-02-01 09:29

src/data/set/image.lean

feat(linear_algebra/affine_space/basis): `reindex` API (#18190) …

Modified set.preimage_injective View on Github →

2022-12-07 20:30

src/data/set/basic.lean

refactor(data/set/basic): move image, preimage, and range to a new file (#17842) …

Modified set.preimage_injective View on Github →

2020-06-27 05:25

src/data/set/basic.lean

feat(set): preliminaries for Haar measure (#3189) …

Added set.preimage_injective View on Github →