Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.embedding.ext

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.extView on Github →
2019-11-07 03:43
src/logic/embedding.lean
feat(extensionality): rename to `ext`; generate `ext` rules for structures (#1645) …
Modified function.embedding.extView on Github →
2019-04-23 20:15
src/logic/embedding.lean
feat(function/embedding): ext and ext_iff (#962)
Added function.embedding.extView on Github →