Commit 2023-12-16 02:09 a5732e8f

View on Github →

chore(ModelTheory/ElementarySubstructures): Split elementary substructures into their own file (#9026) This PR splits the file ModelTheory/ElementaryMaps into two files, moving elementary substructure code into ModelTheory/ElementarySubstructures, to make room for new API on those. Two basic lemmas, FirstOrder.Language.Substructure.realize_boundedFormula_top and FirstOrder.Language.Substructure.realize_formula_top, are instead moved to the file ModelTheory/Substructures.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/ModelTheory/Bundled.lean

Modified Mathlib/ModelTheory/ElementaryMaps.lean

deleted theorem FirstOrder.Language.ElementarySubstructure.coeSubtype

deleted theorem FirstOrder.Language.ElementarySubstructure.coe_top

deleted theorem FirstOrder.Language.ElementarySubstructure.elementarilyEquivalent

deleted theorem FirstOrder.Language.ElementarySubstructure.isElementary

deleted theorem FirstOrder.Language.ElementarySubstructure.mem_top

deleted theorem FirstOrder.Language.ElementarySubstructure.realize_sentence

deleted def FirstOrder.Language.ElementarySubstructure.subtype

deleted theorem FirstOrder.Language.ElementarySubstructure.theory_model_iff

deleted structure FirstOrder.Language.ElementarySubstructure

deleted def FirstOrder.Language.Substructure.IsElementary

deleted theorem FirstOrder.Language.Substructure.isElementary_of_exists

deleted theorem FirstOrder.Language.Substructure.realize_boundedFormula_top

deleted theorem FirstOrder.Language.Substructure.realize_formula_top

deleted def FirstOrder.Language.Substructure.toElementarySubstructure

Created Mathlib/ModelTheory/ElementarySubstructures.lean

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 def FirstOrder.Language.Substructure.IsElementary

added theorem FirstOrder.Language.Substructure.isElementary_of_exists

added def FirstOrder.Language.Substructure.toElementarySubstructure

Modified Mathlib/ModelTheory/Skolem.lean

Modified Mathlib/ModelTheory/Substructures.lean

added theorem FirstOrder.Language.Substructure.realize_boundedFormula_top

added theorem FirstOrder.Language.Substructure.realize_formula_top