Commit 2022-02-08 19:01 4545e31e

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.