define and prove properties of orthocenters with vector algebra #294
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
jjdishere
reviewed
Jan 19, 2024
| @@ -10,7 +11,15 @@ variable {P : Type _} [EuclideanPlane P] | |||
|
|
|||
| def TriangleND.Height1 (tr_nd : TriangleND P) : SegND P := sorry | |||
|
|
|||
| structure IsOrthocenter (tr_nd : TriangleND P) (H : P) : Prop where | |||
| -- this takes care of corner cases such as right triangles, where AH ⟂ BC runs into trouble since A = H | |||
| def IsOrthocenter (tr_nd : TriangleND P) (H : P) : Prop := inner (VEC tr_nd.point₁ H) (VEC tr_nd.point₂ tr_nd.point₃) = (0 : ℝ) ∧ inner (VEC tr_nd.point₂ H) (VEC tr_nd.point₃ tr_nd.point₁) = (0 : ℝ) ∧ inner (VEC tr_nd.point₃ H) (VEC tr_nd.point₁ tr_nd.point₂) = (0 : ℝ) | |||
There was a problem hiding this comment.
- Please write this as a structure
structure IsOrthocenter ... : Prop where
to avoid usage of plural and.
- Is it possible to use
perpendicular, orperp footorLiesOn Height1to define orthocenter? I do hope that there will be a "uniform" way of defining each center of a triangle. This needs a further discussion.
There was a problem hiding this comment.
- Please write a plan file (possibly using overleaf) if you are going to build a whole new file, thank you! You may find some example of plan file in the folder
PlanFiles.
There was a problem hiding this comment.
LiesOn Height1 will work, but the necessary lemmas are not ready yet.
| -- this takes care of corner cases such as right triangles, where AH ⟂ BC runs into trouble since A = H | ||
| def IsOrthocenter (tr_nd : TriangleND P) (H : P) : Prop := inner (VEC tr_nd.point₁ H) (VEC tr_nd.point₂ tr_nd.point₃) = (0 : ℝ) ∧ inner (VEC tr_nd.point₂ H) (VEC tr_nd.point₃ tr_nd.point₁) = (0 : ℝ) ∧ inner (VEC tr_nd.point₃ H) (VEC tr_nd.point₁ tr_nd.point₂) = (0 : ℝ) | ||
|
|
||
| theorem orthocenter_exists (tr : Triangle P) (H : P) (h₁ : inner (VEC tr.point₁ H) (VEC tr.point₂ tr.point₃) = (0 : ℝ)) (h₂ : inner (VEC tr.point₂ H) (VEC tr.point₃ tr.point₁) = (0 : ℝ)) : inner (VEC tr.point₃ H) (VEC tr.point₁ tr.point₂) = (0 : ℝ) := by |
There was a problem hiding this comment.
This theorem could be instead stated as a def that takes in an triangle and output a point. Then check this def do satisfies IsOrthocenter
There was a problem hiding this comment.
This strategy is used in the file AngBisector. Maybe first writing a plan file or discussing directly with me is more time-saving!
There was a problem hiding this comment.
Well, this can be implemented. But surely there is no need to complete everything in one commit?
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.
The definition might not be "geometric" enough but takes care of all corner cases.
Even if we decide upon another definition later, this lemma should still be useful.