Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.embedding.apply_eq_iff_eq

Modification history

2022-01-25 10:49
src/logic/embedding.lean
feat(data/fun_like): define `embedding_like` and `equiv_like` (#10759) …
Modified function.embedding.apply_eq_iff_eqView on Github →
2021-11-28 23:50
src/logic/embedding.lean
chore(logic): allow `Sort*` args in 2 lemmas (#10517)
Modified function.embedding.apply_eq_iff_eqView on Github →
2021-07-16 07:34
src/logic/embedding.lean
feat(logic/embedding): simp lemma for injectivity for embeddings (#7881)
Added function.embedding.apply_eq_iff_eqView on Github →