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(analysis/convex/between): more transitivity variants #17527
Conversation
Add more variants of transitivity lemmas, giving that one endpoint is not equal to the middle point in cases where the hypotheses imply weak betweenness (and we already have the corresponding transitivity lemmas for that), and that one endpoint is not equal to the middle point, but don't imply strict betweenness.
lemma wbtw.trans_left_ne [no_zero_smul_divisors R V] {w x y z : P} (h₁ : wbtw R w y z) | ||
(h₂ : wbtw R w x y) (h : y ≠ z) : x ≠ z := |
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.
This to me reads like you're doing transitivity on the rightmost two elements, so it should rather be
lemma wbtw.trans_left_ne [no_zero_smul_divisors R V] {w x y z : P} (h₁ : wbtw R w y z) | |
(h₂ : wbtw R w x y) (h : y ≠ z) : x ≠ z := | |
lemma wbtw.trans_right_ne [no_zero_smul_divisors R V] {w x y z : P} (h₁ : wbtw R w x y) | |
(h₂ : wbtw R w y z) (h : y ≠ z) : x ≠ z := |
but I see you already have been using another in the rest of the file.
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.
Thanks 🎉
bors merge
(If left/right needs to be swapped, then this should be done for the entire file/directory in another PR.)
Add more variants of transitivity lemmas, giving that one endpoint is not equal to the middle point in cases where the hypotheses imply weak betweenness (and we already have the corresponding transitivity lemmas for that), and that one endpoint is not equal to the middle point, but don't imply strict betweenness.
Pull request successfully merged into master. Build succeeded: |
Add more variants of transitivity lemmas, giving that one endpoint is not equal to the middle point in cases where the hypotheses imply weak betweenness (and we already have the corresponding transitivity lemmas for that), and that one endpoint is not equal to the middle point, but don't imply strict betweenness.