Commit 2023-03-30 05:03 374abad1

View on Github →

feat: port ModelTheory.Basic (#2296)

Estimated changes

Modified Mathlib.lean

Created Mathlib/ModelTheory/Basic.lean

added def Embedding.empty

added def Equiv.empty

added def Equiv.inducedStructure

added def Equiv.inducedStructureEquiv

added theorem Equiv.toEquiv_inducedStructureEquiv

added theorem Equiv.toFun_inducedStructureEquiv

added theorem Equiv.toFun_inducedStructureEquiv_Symm

added theorem FirstOrder.Language.Embedding.coeFn_ofInjective

added theorem FirstOrder.Language.Embedding.coe_injective

added theorem FirstOrder.Language.Embedding.coe_toHom

added def FirstOrder.Language.Embedding.comp

added theorem FirstOrder.Language.Embedding.comp_apply

added theorem FirstOrder.Language.Embedding.comp_assoc

added theorem FirstOrder.Language.Embedding.comp_toHom

added theorem FirstOrder.Language.Embedding.ext

added theorem FirstOrder.Language.Embedding.ext_iff

added theorem FirstOrder.Language.Embedding.injective

added theorem FirstOrder.Language.Embedding.map_constants

added theorem FirstOrder.Language.Embedding.map_fun

added theorem FirstOrder.Language.Embedding.map_rel

added def FirstOrder.Language.Embedding.ofInjective

added theorem FirstOrder.Language.Embedding.ofInjective_toHom

added def FirstOrder.Language.Embedding.refl

added theorem FirstOrder.Language.Embedding.refl_apply

added def FirstOrder.Language.Embedding.toHom

added structure FirstOrder.Language.Embedding

added theorem FirstOrder.Language.Equiv.apply_symm_apply

added theorem FirstOrder.Language.Equiv.bijective

added theorem FirstOrder.Language.Equiv.coe_injective

added theorem FirstOrder.Language.Equiv.coe_toEmbedding

added theorem FirstOrder.Language.Equiv.coe_toHom

added def FirstOrder.Language.Equiv.comp

added theorem FirstOrder.Language.Equiv.comp_apply

added theorem FirstOrder.Language.Equiv.comp_assoc

added theorem FirstOrder.Language.Equiv.ext

added theorem FirstOrder.Language.Equiv.ext_iff

added theorem FirstOrder.Language.Equiv.injective

added theorem FirstOrder.Language.Equiv.map_constants

added theorem FirstOrder.Language.Equiv.map_fun

added theorem FirstOrder.Language.Equiv.map_rel

added def FirstOrder.Language.Equiv.refl

added theorem FirstOrder.Language.Equiv.refl_apply

added theorem FirstOrder.Language.Equiv.surjective

added def FirstOrder.Language.Equiv.symm

added theorem FirstOrder.Language.Equiv.symm_apply_apply

added def FirstOrder.Language.Equiv.toEmbedding

added theorem FirstOrder.Language.Equiv.toEmbedding_toHom

added def FirstOrder.Language.Equiv.toHom

added structure FirstOrder.Language.Equiv

added def FirstOrder.Language.Hom.comp

added theorem FirstOrder.Language.Hom.comp_apply

added theorem FirstOrder.Language.Hom.comp_assoc

added theorem FirstOrder.Language.Hom.ext

added theorem FirstOrder.Language.Hom.ext_iff

added def FirstOrder.Language.Hom.id

added theorem FirstOrder.Language.Hom.id_apply

added theorem FirstOrder.Language.Hom.map_constants

added theorem FirstOrder.Language.Hom.map_fun

added theorem FirstOrder.Language.Hom.map_rel

added theorem FirstOrder.Language.Hom.toFun_eq_coe

added structure FirstOrder.Language.Hom

added theorem FirstOrder.Language.HomClass.map_constants

added def FirstOrder.Language.HomClass.strongHomClassOfIsAlgebraic

added def FirstOrder.Language.HomClass.toHom

added def FirstOrder.Language.RelMap₂

added def FirstOrder.Language.StrongHomClass.toEmbedding

added def FirstOrder.Language.StrongHomClass.toEquiv

added theorem FirstOrder.Language.Structure.funMap_apply₀

added theorem FirstOrder.Language.Structure.funMap_apply₁

added theorem FirstOrder.Language.Structure.funMap_apply₂

added theorem FirstOrder.Language.Structure.relMap_apply₁

added theorem FirstOrder.Language.Structure.relMap_apply₂

added def FirstOrder.Language.Symbols

added def FirstOrder.Language.card

added theorem FirstOrder.Language.card_eq_card_functions_add_card_relations

added theorem FirstOrder.Language.card_functions_sum

added theorem FirstOrder.Language.card_mk₂

added theorem FirstOrder.Language.card_relations_sum

added theorem FirstOrder.Language.card_sum

added def FirstOrder.Language.constantMap

added theorem FirstOrder.Language.constants_mk₂

added theorem FirstOrder.Language.empty.nonempty_embedding_iff

added theorem FirstOrder.Language.empty.nonempty_equiv_iff

added theorem FirstOrder.Language.empty_card

added theorem FirstOrder.Language.funMap_eq_coe_constants

added theorem FirstOrder.Language.funMap_sum_inl

added theorem FirstOrder.Language.funMap_sum_inr

added def FirstOrder.Language.funMap₂

added def FirstOrder.Language.inhabited.trivialStructure

added theorem FirstOrder.Language.nonempty_of_nonempty_constants

added theorem FirstOrder.Language.relMap_sum_inl

added theorem FirstOrder.Language.relMap_sum_inr

added theorem FirstOrder.Language.toEmbedding_embedding_empty

added theorem FirstOrder.Language.toEquiv_equiv_empty

added theorem FirstOrder.Language.toFun_embedding_empty

added theorem FirstOrder.Language.toFun_equiv_empty

added structure FirstOrder.Language

added theorem FirstOrder.Sequence₂.lift_mk

added theorem FirstOrder.Sequence₂.sum_card

added def FirstOrder.Sequence₂

added def Function.emptyHom