Mathlib v3 is deprecated. Go to Mathlib v4

Theorem set.mem_image_of_injective

Modification history

2021-09-08 14:01
src/data/set/basic.lean
feat(data/(fin)set/basic): `image` and `mem` lemmas (#9031) …
Deleted set.mem_image_of_injectiveView on Github →
2017-12-31 16:53
data/set/basic.lean
feat(data/ordinal): is_normal, omin, power/log, CNF, indecomposables, …
Modified set.mem_image_of_injectiveView on Github →
2017-12-08 17:29
data/set/basic.lean
refactor(algebra/module): split of type constructions and move quotient, subtype and linear_map to their own theories in algebra/linear_algebra
Added set.mem_image_of_injectiveView on Github →