mathlib

2508cbd9 - feat(model_theory/basic.lean): Elementary embeddings and elementary substructures (#11089)

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