mathlib

4545e31e - feat(model_theory/substructures): More operations on substructures (#11906)

feat(model_theory/substructures): More operations on substructures (#11906) Defines the substructure `first_order.language.hom.range`. Defines the homomorphisms `first_order.language.hom.dom_restrict` and `first_order.language.hom.cod_restrict`, and the embeddings `first_order.language.embedding.dom_restrict`, `first_order.language.embedding.cod_restrict` which restrict the domain or codomain of a first-order hom or embedding to a substructure. Defines the embedding `first_order.language.substructure.inclusion` between nested substructures.