[Merged by Bors] - feat(geometry/euclidean/monge_point): lemmas on altitudes and orthocenter #4179
Conversation
…nter Add more lemmas about altitudes of a simplex and the orthocenter of a triangle. Some of these are just building out basic API that's mathemtically trivial (e.g. showing that the altitude as defined is a one-dimensional affine subspace and providing an explicit form of its direction), while the results on the orthocenter have some geometrical content that's part of the preparation for defining and proving basic properties of orthocentric systems.
| necessarily listed in the same order). Then the orthocenter of `t₂` | ||
| is the vertex of `t₁` that was replaced. -/ | ||
| lemma orthocenter_replace_orthocenter_eq_point {t₁ t₂ : triangle ℝ P} {i₁ i₂ i₃ j₁ j₂ j₃ : fin 3} | ||
| (hi₁₂ : i₁ ≠ i₂) (hi₁₃ : i₁ ≠ i₃) (hi₂₃ : i₂ ≠ i₃) (hj₁₂ : j₁ ≠ j₂) (hj₁₃ : j₁ ≠ j₃) |
There was a problem hiding this comment.
I wonder if there's a bundled way to state (hi₁₂ : i₁ ≠ i₂) (hi₁₃ : i₁ ≠ i₃) (hi₂₃ : i₂ ≠ i₃)...
There was a problem hiding this comment.
Well, it's possible to write things such as (hi : function.injective ![i₁, i₂, i₃]), but I think for most cases of concrete choices of indices it will be more convenient to produce the three ≠ hypotheses. (The general principle that can be seen at work in these lemmas is that the manipulations involved in proving something for general n tend to be more convenient than those involved in proving something specific to the case of 3.)
There was a problem hiding this comment.
Using list.pairwise you can say [i₁, i₂, i₃].pairwise (≠)
There was a problem hiding this comment.
If what you have when using this sort of result is a list or a function from fin 3 or anything like that, in which all three indices play exactly the same role, the bundled forms make sense. But I don't think that's the main use case for such lemmas (indeed, in this lemma, the indices don't all play the same role; one is the vertex being replaced, the other two are the vertices not being replaced). When the indices don't all play the same role, that's liable to mean that inequality of different indices may be derived in different ways (possibly from norm_num, when the indices are 0, 1 and 2, possibly from dec_trivial, when some of them are arbitrary fin 3 values different from one or two such values passed into a lemma using this one, for example), making three separate hypotheses more convenient to pass to this lemma than one bundled hypothesis.
There was a problem hiding this comment.
Note that @shingtaklam1324's version is straightforward to produce with
import data.list.pairwise
example {α : Type} {i₁ i₂ i₃ : α} (hi₁₂ : i₁ ≠ i₂) (hi₁₃ : i₁ ≠ i₃) (hi₂₃ : i₂ ≠ i₃) : [i₁, i₂, i₃].pairwise (≠) := by tidy; exact list.pairwise.nil
It looks to me like pairwise.nil is missing a simp lemma (edit: #4254)
There was a problem hiding this comment.
With #4281, the proof above is just by simp - so in principle a caller of orthocenter_replace_orthocenter_eq_point could just use refine orthocenter_replace_orthocenter_eq_point _ h₁ h₂ h₃, simp, and they'd end up at the three hypotheses you list here. Up to you whether you want to explore this further.
There was a problem hiding this comment.
I tend to think that alternative options for how to express that these indices are distinct would best be explored once we have users of orthocenter_replace_orthocenter_eq_point. (I have a definition and some basic properties of orthocentric systems, but as well as this PR those properties depend on some definitions / lemmas about collinearity that I want to rework before PRing them.)
github-actions
bot
added
ready-to-merge
…nter (#4179) Add more lemmas about altitudes of a simplex and the orthocenter of a triangle. Some of these are just building out basic API that's mathematically trivial (e.g. showing that the altitude as defined is a one-dimensional affine subspace and providing an explicit form of its direction), while the results on the orthocenter have some geometrical content that's part of the preparation for defining and proving basic properties of orthocentric systems.
|
Build failed (retrying...): |
…nter (#4179) Add more lemmas about altitudes of a simplex and the orthocenter of a triangle. Some of these are just building out basic API that's mathematically trivial (e.g. showing that the altitude as defined is a one-dimensional affine subspace and providing an explicit form of its direction), while the results on the orthocenter have some geometrical content that's part of the preparation for defining and proving basic properties of orthocentric systems.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Add more lemmas about altitudes of a simplex and the orthocenter of a
triangle. Some of these are just building out basic API that's
mathematically trivial (e.g. showing that the altitude as defined is a
one-dimensional affine subspace and providing an explicit form of its
direction), while the results on the orthocenter have some geometrical
content that's part of the preparation for defining and proving basic
properties of orthocentric systems.