New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(model_theory/substructures): More operations on substructures #11906
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM, just some minor comments
bors d+
✌️ awainverse can now approve this pull request. To approve and merge a pull request, simply reply with |
bors d+ |
✌️ awainverse can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
…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.
Pull request successfully merged into master. Build succeeded: |
Defines the substructure
first_order.language.hom.range
.Defines the homomorphisms
first_order.language.hom.dom_restrict
andfirst_order.language.hom.cod_restrict
, and the embeddingsfirst_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.