Commit 2022-12-14 15:48 2d122651

View on Github →

feat port: Logic.Equiv.Embedding (#1021) ee0c179cd3c8a45aa5bffbf1b41d8dbede452865

Estimated changes

Modified Mathlib.lean

Created Mathlib/Logic/Equiv/Embedding.lean

added def Equiv.codRestrict

added def Equiv.prodEmbeddingDisjointEquivSigmaEmbeddingRestricted

added def Equiv.sumEmbeddingEquivProdEmbeddingDisjoint

added def Equiv.sumEmbeddingEquivSigmaEmbeddingRestricted

added def Equiv.uniqueEmbeddingEquivResult