Commit 2023-05-13 13:53 26d57280

View on Github →

feat: port ModelTheory.ElementaryMaps (#3931)

Estimated changes

Modified Mathlib.lean

Created Mathlib/ModelTheory/ElementaryMaps.lean

added theorem FirstOrder.Language.ElementaryEmbedding.coe_injective

added theorem FirstOrder.Language.ElementaryEmbedding.coe_toEmbedding

added theorem FirstOrder.Language.ElementaryEmbedding.coe_toHom

added def FirstOrder.Language.ElementaryEmbedding.comp

added theorem FirstOrder.Language.ElementaryEmbedding.comp_apply

added theorem FirstOrder.Language.ElementaryEmbedding.comp_assoc

added theorem FirstOrder.Language.ElementaryEmbedding.elementarilyEquivalent

added theorem FirstOrder.Language.ElementaryEmbedding.ext

added theorem FirstOrder.Language.ElementaryEmbedding.ext_iff

added theorem FirstOrder.Language.ElementaryEmbedding.injective

added theorem FirstOrder.Language.ElementaryEmbedding.map_boundedFormula

added theorem FirstOrder.Language.ElementaryEmbedding.map_constants

added theorem FirstOrder.Language.ElementaryEmbedding.map_formula

added theorem FirstOrder.Language.ElementaryEmbedding.map_fun

added theorem FirstOrder.Language.ElementaryEmbedding.map_rel

added theorem FirstOrder.Language.ElementaryEmbedding.map_sentence

added def FirstOrder.Language.ElementaryEmbedding.ofModelsElementaryDiagram

added def FirstOrder.Language.ElementaryEmbedding.refl

added theorem FirstOrder.Language.ElementaryEmbedding.refl_apply

added theorem FirstOrder.Language.ElementaryEmbedding.theory_model_iff

added def FirstOrder.Language.ElementaryEmbedding.toEmbedding

added theorem FirstOrder.Language.ElementaryEmbedding.toEmbedding_toHom

added def FirstOrder.Language.ElementaryEmbedding.toHom

added structure FirstOrder.Language.ElementaryEmbedding

added theorem FirstOrder.Language.ElementarySubstructure.coeSubtype

added theorem FirstOrder.Language.ElementarySubstructure.coe_top

added theorem FirstOrder.Language.ElementarySubstructure.elementarilyEquivalent

added theorem FirstOrder.Language.ElementarySubstructure.isElementary

added theorem FirstOrder.Language.ElementarySubstructure.mem_top

added theorem FirstOrder.Language.ElementarySubstructure.realize_sentence

added def FirstOrder.Language.ElementarySubstructure.subtype

added theorem FirstOrder.Language.ElementarySubstructure.theory_model_iff

added structure FirstOrder.Language.ElementarySubstructure

added theorem FirstOrder.Language.Embedding.isElementary_of_exists

added def FirstOrder.Language.Embedding.toElementaryEmbedding

added theorem FirstOrder.Language.Equiv.coe_toElementaryEmbedding

added def FirstOrder.Language.Equiv.toElementaryEmbedding

added theorem FirstOrder.Language.Equiv.toElementaryEmbedding_toEmbedding

added def FirstOrder.Language.Substructure.IsElementary

added theorem FirstOrder.Language.Substructure.isElementary_of_exists

added theorem FirstOrder.Language.Substructure.realize_boundedFormula_top

added theorem FirstOrder.Language.Substructure.realize_formula_top

added def FirstOrder.Language.Substructure.toElementarySubstructure

added theorem FirstOrder.Language.realize_term_substructure