triangle inequality for naturals and integers #177
Merged
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
|
Thanks for your contribution. Will have a look now. |
martinescardo
approved these changes
Sep 7, 2023
|
Waiting for the checks to complete to merge. |
|
You should also add yourself to the list of contributors in the top-level README file. |
|
You have added the year of your contribution. Please also add the day and month. |
|
When you have a chance, please to a pull request to address the above issues. Thanks. |
|
@martinescardo I will work on this clean-up over the weekend, thank you for accepting my work! |
|
Done with all these, I submitted a new PR to amend all these at the end of last week. Thank you! |
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.
On Dr. Escardo's invitation from mathstodon, I am contributing my proof of the triangle inequality in the Naturals and the Integers. In the Naturals, I define a new Absolute Difference operation and prove some elementary lemmas. I then add associated lemmas for Absolute Difference to the Natural Order lemmas, proving the triangle inequality on the way for the naturals under this operation. I then prove some useful lemmas for Absolute Value in the Integers related to this new operation, and conclude by proving the triangle inequality in the Integer Order file (for both abs and adding a translated lemma to absZ for convenience).