Commit 2022-12-14 03:08 d49808fa

View on Github →

feat port: logic.embedding.set (#986) fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e

Estimated changes

Modified Mathlib.lean

Created Mathlib/Logic/Embedding/Set.lean

added theorem Equiv.asEmbedding_range

added def Function.Embedding.codRestrict

added theorem Function.Embedding.codRestrict_apply

added def Function.Embedding.coeWithTop

added def Function.Embedding.optionElim

added def Function.Embedding.optionEmbeddingEquiv

added def Set.embeddingOfSubset

added def subtypeOrEquiv

added theorem subtypeOrEquiv_symm_inl

added theorem subtypeOrEquiv_symm_inr