Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-08 19:13 39406bb9

View on Github →

feat(model_theory/basic): First-order languages, structures, homomorphisms, embeddings, and equivs (#7754) Defines the following notions from first-order logic:

languages
structures
homomorphisms
embeddings
equivalences (isomorphisms) The definitions of languages and structures take inspiration from the Flypitch project.

Estimated changes

Modified docs/references.bib

Created src/model_theory/basic.lean

added def first_order.language.const

added theorem first_order.language.embedding.coe_injective

added theorem first_order.language.embedding.coe_to_hom

added def first_order.language.embedding.comp

added theorem first_order.language.embedding.comp_apply

added theorem first_order.language.embedding.comp_assoc

added theorem first_order.language.embedding.ext

added theorem first_order.language.embedding.ext_iff

added theorem first_order.language.embedding.injective

added theorem first_order.language.embedding.map_fun

added theorem first_order.language.embedding.map_rel

added def first_order.language.embedding.refl

added theorem first_order.language.embedding.refl_apply

added def first_order.language.embedding.to_hom

added def first_order.language.empty

added theorem first_order.language.equiv.coe_injective

added theorem first_order.language.equiv.coe_to_embedding

added theorem first_order.language.equiv.coe_to_hom

added def first_order.language.equiv.comp

added theorem first_order.language.equiv.comp_apply

added theorem first_order.language.equiv.comp_assoc

added theorem first_order.language.equiv.ext

added theorem first_order.language.equiv.ext_iff

added theorem first_order.language.equiv.injective

added theorem first_order.language.equiv.map_fun

added theorem first_order.language.equiv.map_rel

added def first_order.language.equiv.refl

added theorem first_order.language.equiv.refl_apply

added def first_order.language.equiv.symm

added def first_order.language.equiv.to_embedding

added theorem first_order.language.equiv.to_embedding_to_hom

added def first_order.language.equiv.to_hom

added theorem first_order.language.hom.coe_injective

added def first_order.language.hom.comp

added theorem first_order.language.hom.comp_apply

added theorem first_order.language.hom.comp_assoc

added theorem first_order.language.hom.ext

added theorem first_order.language.hom.ext_iff

added def first_order.language.hom.id

added theorem first_order.language.hom.id_apply

added theorem first_order.language.hom.map_fun

added theorem first_order.language.hom.map_rel

added theorem first_order.language.hom.to_fun_eq_coe

added structure first_order.language