Commit 2023-04-12 21:55 28d9dc68

View on Github →

feat: port ModelTheory.LanguageMap (#3194)

Estimated changes

Modified Mathlib.lean

Created Mathlib/ModelTheory/LanguageMap.lean

added def FirstOrder.Language.LEquiv.addEmptyConstants

added structure FirstOrder.Language.LEquiv

added theorem FirstOrder.Language.LHom.Injective.isExpansionOn_default

added def FirstOrder.Language.LHom.addConstants

added def FirstOrder.Language.LHom.comp

added theorem FirstOrder.Language.LHom.comp_assoc

added theorem FirstOrder.Language.LHom.comp_id

added theorem FirstOrder.Language.LHom.comp_sumElim

added def FirstOrder.Language.LHom.constantsOnMap

added theorem FirstOrder.Language.LHom.funMap_sumInl

added theorem FirstOrder.Language.LHom.funMap_sumInr

added theorem FirstOrder.Language.LHom.id_comp

added theorem FirstOrder.Language.LHom.map_constants_comp_sumInl

added theorem FirstOrder.Language.LHom.map_onFunction

added theorem FirstOrder.Language.LHom.map_onRelation

added theorem FirstOrder.Language.LHom.mk₂_funext

added def FirstOrder.Language.LHom.reduct

added theorem FirstOrder.Language.LHom.sumElim_comp_inl

added theorem FirstOrder.Language.LHom.sumElim_comp_inr

added theorem FirstOrder.Language.LHom.sumElim_inl_inr

added theorem FirstOrder.Language.LHom.sumInl_injective

added theorem FirstOrder.Language.LHom.sumInr_injective

added def FirstOrder.Language.LHom.sumMap

added theorem FirstOrder.Language.LHom.sumMap_comp_inl

added theorem FirstOrder.Language.LHom.sumMap_comp_inr

added structure FirstOrder.Language.LHom

added theorem FirstOrder.Language.card_constantsOn

added theorem FirstOrder.Language.card_withConstants

added theorem FirstOrder.Language.coe_con

added def FirstOrder.Language.constantsOn.structure

added def FirstOrder.Language.constantsOn

added theorem FirstOrder.Language.constantsOnMap_isExpansionOn

added theorem FirstOrder.Language.constantsOn_constants

added def FirstOrder.Language.lhomWithConstants

added def FirstOrder.Language.lhomWithConstantsMap

added theorem FirstOrder.Language.lhomWithConstants_injective

added def FirstOrder.Language.withConstants

added theorem FirstOrder.Language.withConstants_funMap_sum_inl

added theorem FirstOrder.Language.withConstants_funMap_sum_inr

added theorem FirstOrder.Language.withConstants_relMap_sum_inl