Commit 2022-11-28 01:58 6cf4e3ae

View on Github →

port logic.embedding.basic (#700) From mathlib3port: e50b8c261b0a000b806ec0e1356b41945eda61f7

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Logic/Basic.lean

added theorem eq_ite_iff

Created Mathlib/Logic/Embedding/Basic.lean

added def Equiv.asEmbedding

added theorem Equiv.coe_toEmbedding

added def Equiv.embeddingCongr

added theorem Equiv.embeddingCongr_apply_trans

added theorem Equiv.embeddingCongr_refl

added theorem Equiv.embeddingCongr_symm

added theorem Equiv.embeddingCongr_trans

added theorem Equiv.refl_toEmbedding

added def Equiv.subtypeInjectiveEquivEmbedding

added theorem Equiv.toEmbedding_apply

added theorem Equiv.trans_toEmbedding

added def Function.Embedding.Simps.apply

added theorem Function.Embedding.apply_eq_iff_eq

added def Function.Embedding.arrowCongrRight

added theorem Function.Embedding.arrowCongrRight_apply

added theorem Function.Embedding.coeFn_mk

added theorem Function.Embedding.coe_injective

added theorem Function.Embedding.coe_prodMap

added theorem Function.Embedding.coe_quotientOut

added theorem Function.Embedding.coe_subtype

added theorem Function.Embedding.coe_sumMap

added theorem Function.Embedding.equiv_symm_toEmbedding_trans_toEmbedding

added theorem Function.Embedding.equiv_toEmbedding_trans_symm_toEmbedding

added theorem Function.Embedding.ext

added theorem Function.Embedding.ext_iff

added def Function.Embedding.inl

added def Function.Embedding.inr

added theorem Function.Embedding.mk_coe

added def Function.Embedding.optionMap

added def Function.Embedding.piCongrRight

added def Function.Embedding.pprodMap

added def Function.Embedding.prodMap

added def Function.Embedding.punit

added def Function.Embedding.sectl

added def Function.Embedding.sectr

added def Function.Embedding.setValue

added theorem Function.Embedding.setValue_eq

added def Function.Embedding.sigmaMap

added def Function.Embedding.sigmaMk

added def Function.Embedding.subtype

added def Function.Embedding.sumMap

added theorem Function.Embedding.swap_apply

added theorem Function.Embedding.swap_comp

added theorem Function.Embedding.toFun_eq_coe

added structure Function.Embedding

added def Subtype.impEmbedding

added def subtypeOrLeftEmbedding

added theorem subtypeOrLeftEmbedding_apply_left

added theorem subtypeOrLeftEmbedding_apply_right

Created lean_packages/Qq

Created lean_packages/aesop

Created lean_packages/std