Mathlib v3 is deprecated. Go to Mathlib v4

Def subtype_or_left_embedding

Modification history

2021-08-06 15:53
src/logic/embedding.lean
feat(logic/embedding): subtype_or_{embedding,equiv} (#8489) …
Added subtype_or_left_embeddingView on Github →