-
Notifications
You must be signed in to change notification settings - Fork 298
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] - refactor(analysis/convex/basic): rewrite a few proofs #13658
Conversation
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
* prove that a closed segment is the union of the corresponding open segment and the endpoints; * use this lemma to golf some proofs; * make the "field" argument of `mem_open_segment_of_ne_left_right` implicit. * use section variables.
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 a lot! This looks nice.
refine and_congr_right (λ hxA, forall₄_congr $ λ x₁ h₁ x₂ h₂, _), | ||
split, |
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.
You can even save another two lines like this.
refine and_congr_right (λ hxA, forall₄_congr $ λ x₁ h₁ x₂ h₂, _), | |
split, | |
refine and_congr_right (λ hxA, forall₄_congr $ λ x₁ h₁ x₂ h₂, ⟨_, λ H hx, _⟩), |
lemma mem_open_segment_of_ne_left_right {x y z : E} (hx : x ≠ z) (hy : y ≠ z) | ||
(hz : z ∈ [x -[𝕜] y]) : | ||
z ∈ open_segment 𝕜 x y := | ||
lemma insert_endpoints_open_segment (x y : E) : |
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.
Not sure about the name of that one. I think it's okay, but I would have expected some thing like _left_right
instead of _endpoints
.
Pull request successfully merged into master. Build succeeded: |
mem_open_segment_of_ne_left_right
implicit.