[Merged by Bors] - feat(model_theory/basic): Substructures

[awainverse]

Defines substructures of first-order structures

---

• depends on: [Merged by Bors] - feat(model_theory/basic): First-order languages, structures, homomorphisms, embeddings, and equivs #7754

[github-actions]

🎉 Great news! Looks like all the dependencies have been resolved:

• [Merged by Bors] - feat(model_theory/basic): First-order languages, structures, homomorphisms, embeddings, and equivs #7754

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

[Vierkantor]

It might be worth the effort to instead define closure as a lower_adjoint (coe : L.substructure M → set M) and get a lot of the following lemmas (and quite a few additional ones!) for free. However, lower_adjoint doesn't seem to be used yet in mathlib, so it's fine if you want to leave that to someone else.

[awainverse]

Done!

There's probably a better way to connect lower_adjoint to gi, but it does require an additional assumption (that the upper adjoint has the property that u x <= u y implies x <= y). I think this could at least be done at the level of set_like, but perhaps that's for a different PR.

[Vierkantor]

Thanks!

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests