fixes #1301 #1303
Merged
fixes #1301 #1303
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
- add relation_scope
affeldt-aist
added
the
renaming/refactoring 🔧
zstone1
approved these changes
Aug 24, 2024
theories/normedtype.v
Outdated
| @@ -3622,10 +3621,10 @@ move/(_ (globally [set fg | fg.1 = fg.2])); apply; split. | |||
| exact: ury_base_refl. | |||
| Qed. | |||
|
|
|||
| Local Lemma set_prod_invK (K : set (T * T)) : (K^-1^-1)%classic = K. | |||
| Local Lemma set_prod_invK (K : set (T * T)) : K^-1^-1 = K. | |||
There was a problem hiding this comment.
If we're cleaning things up, shouldn't this live in classical_set rather than as a local lemma hwre?
There was a problem hiding this comment.
Yes, I missed it. Thanks.
There was a problem hiding this comment.
I also added a definition for the diagonal, since the notation was repeated several times.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
fixes #1301
Motivation for this change
While fixing the documentation for the notation
\;, I realized that the notation for the inverseof a relation was locally defined in three files. Since it seems to be used always along with
\;,I added a
relation_scopethat can be open in sections dealing with uniform spaces. I thinkit is quite natural as it does not cause clashes with the already overloaded
^-1notation andalso because it reduces the clutter in statements.
Checklist
CHANGELOG_UNRELEASED.mdReference: How to document
Reminder to reviewers