[Merged by Bors] - chore(ModelTheory/ElementarySubstructures): Split elementary substructures into their own file #9026
Conversation
awainverse
added
awaiting-review
| -- See note [lower instance priority] | ||
| instance (priority := 100) MeasurableDiv.toMeasurableInv [MeasurableSpace α] [Group α] | ||
| [MeasurableDiv α] : MeasurableInv α where | ||
| measurable_inv := by simpa using measurable_const_div (1 : α) | ||
|
|
There was a problem hiding this comment.
These look unrelated to the current PR; perhaps merging master will make them go away?
There was a problem hiding this comment.
Yes, thanks. Now only model theory files are affected.
|
|
||
| /-- The substructure `M` of the structure `M` is elementary. -/ | ||
| instance instTop : Top (L.ElementarySubstructure M) := | ||
| ⟨⟨⊤, fun _ _ _ => (Substructure.realize_formula_top _ _).symm⟩⟩ |
There was a problem hiding this comment.
This proof grew two underscores; was that deliberate, or should the arguments to realize_formula_top have been kept implicit?
If it was deliberate, please put it in the PR description.
bors d+
There was a problem hiding this comment.
It was not deliberate - I have made those variables implicit again.
In fact, I have now moved those two lemmas to the Substructures file, as I think they really belong there. I will adjust the PR description accordingly.
|
✌️ awainverse can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
…tures into their own file (#9026) This PR splits the file `ModelTheory/ElementaryMaps` into two files, moving elementary substructure code into `ModelTheory/ElementarySubstructures`, to make room for new API on those. Two basic lemmas, `FirstOrder.Language.Substructure.realize_boundedFormula_top` and `FirstOrder.Language.Substructure.realize_formula_top`, are instead moved to the file `ModelTheory/Substructures`. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
…tures into their own file (#9026) This PR splits the file `ModelTheory/ElementaryMaps` into two files, moving elementary substructure code into `ModelTheory/ElementarySubstructures`, to make room for new API on those. Two basic lemmas, `FirstOrder.Language.Substructure.realize_boundedFormula_top` and `FirstOrder.Language.Substructure.realize_formula_top`, are instead moved to the file `ModelTheory/Substructures`. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>
This PR splits the file
ModelTheory/ElementaryMapsinto two files, moving elementary substructure code intoModelTheory/ElementarySubstructures, to make room for new API on those.Two basic lemmas,
FirstOrder.Language.Substructure.realize_boundedFormula_topandFirstOrder.Language.Substructure.realize_formula_top, are instead moved to the fileModelTheory/Substructures.