Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-01 11:04 2508cbd9

View on Github →

feat(model_theory/basic.lean): Elementary embeddings and elementary substructures (#11089) Defines elementary embeddings between structures Defines when substructures are elementary Provides lemmas about preservation of realizations of terms and formulas under various maps

Estimated changes

Modified src/model_theory/basic.lean

added def first_order.language.bounded_formula.relabel

added theorem first_order.language.embedding.realize_term

added structure first_order.language.embedding

added theorem first_order.language.equiv.apply_symm_apply

added theorem first_order.language.equiv.realize_bounded_formula

added theorem first_order.language.equiv.realize_term

added theorem first_order.language.equiv.symm_apply_apply

added structure first_order.language.equiv

added def first_order.language.formula.equal

added def first_order.language.formula.graph

added theorem first_order.language.hom.realize_term

added structure first_order.language.hom

added theorem first_order.language.realize_bounded_formula_relabel

added theorem first_order.language.realize_bounded_formula_top

added theorem first_order.language.realize_equal

added theorem first_order.language.realize_formula_equiv

added theorem first_order.language.realize_formula_relabel

added theorem first_order.language.realize_graph

added theorem first_order.language.realize_term_relabel

added theorem first_order.language.realize_term_substructure

added theorem first_order.language.substructure.coe_top_equiv

added def first_order.language.substructure.top_equiv

added def first_order.language.term.relabel

Created src/model_theory/elementary_maps.lean

added theorem first_order.language.elementary_embedding.coe_injective

added theorem first_order.language.elementary_embedding.coe_to_embedding

added theorem first_order.language.elementary_embedding.coe_to_hom

added def first_order.language.elementary_embedding.comp

added theorem first_order.language.elementary_embedding.comp_apply

added theorem first_order.language.elementary_embedding.comp_assoc

added theorem first_order.language.elementary_embedding.ext

added theorem first_order.language.elementary_embedding.ext_iff

added theorem first_order.language.elementary_embedding.injective

added theorem first_order.language.elementary_embedding.map_const

added theorem first_order.language.elementary_embedding.map_formula

added theorem first_order.language.elementary_embedding.map_fun

added theorem first_order.language.elementary_embedding.map_rel

added def first_order.language.elementary_embedding.refl

added theorem first_order.language.elementary_embedding.refl_apply

added def first_order.language.elementary_embedding.to_embedding

added theorem first_order.language.elementary_embedding.to_embedding_to_hom

added def first_order.language.elementary_embedding.to_hom

added structure first_order.language.elementary_embedding

added theorem first_order.language.elementary_substructure.coe_subtype

added theorem first_order.language.elementary_substructure.coe_top

added theorem first_order.language.elementary_substructure.is_elementary

added theorem first_order.language.elementary_substructure.mem_top

added def first_order.language.elementary_substructure.subtype

added structure first_order.language.elementary_substructure

added theorem first_order.language.equiv.coe_to_elementary_embedding

added def first_order.language.equiv.to_elementary_embedding

added theorem first_order.language.equiv.to_elementary_embedding_to_embedding

added def first_order.language.substructure.is_elementary