feat(Geometry/Euclidean/Angle/Incenter): unoriented angle bisection#32282
Open
jsm28 wants to merge 251 commits into
Open
feat(Geometry/Euclidean/Angle/Incenter): unoriented angle bisection#32282jsm28 wants to merge 251 commits into
jsm28 wants to merge 251 commits into
Conversation
… and bisection lemmas
Add lemmas
```lean
lemma oangle_eq_neg_of_angle_eq_of_sign_eq_neg {w x y z : V}
(h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z)
(hs : (o.oangle w x).sign = -(o.oangle y z).sign) : o.oangle w x = -o.oangle y z := by
```
and
```lean
lemma angle_eq_iff_oangle_eq_neg_of_sign_eq_neg {w x y z : V} (hw : w ≠ 0) (hx : x ≠ 0)
(hy : y ≠ 0) (hz : z ≠ 0) (hs : (o.oangle w x).sign = -(o.oangle y z).sign) :
InnerProductGeometry.angle w x = InnerProductGeometry.angle y z ↔
o.oangle w x = -o.oangle y z := by
```
and similar affine versions, corresponding to such lemmas that already
exist when the signs are equal rather than negations of each other.
Deduce lemmas relating oriented and unoriented versions of angle
bisection:
```lean
lemma angle_eq_iff_oangle_eq_or_sameRay {x y z : V} (hx : x ≠ 0) (hz : z ≠ 0) :
InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔
o.oangle x y = o.oangle y z ∨ SameRay ℝ x z := by
```
and
```lean
lemma angle_eq_iff_oangle_eq_or_wbtw {p₁ p₂ p₃ p₄ : P} (hp₁ : p₁ ≠ p₂) (hp₄ : p₄ ≠ p₂) :
∠ p₁ p₂ p₃ = ∠ p₃ p₂ p₄ ↔ ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ ∨ Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁ := by
```
… equal distance
Add a lemma
```lean
lemma dist_orthogonalProjection_eq_iff_oangle_eq {p p' : P} {s₁ s₂ : AffineSubspace ℝ P}
[s₁.direction.HasOrthogonalProjection] [s₂.direction.HasOrthogonalProjection]
(hp' : p' ∈ s₁ ⊓ s₂)
(hne : haveI : Nonempty s₁ := ⟨p', hp'.1⟩; haveI : Nonempty s₂ := ⟨p', hp'.2⟩;
(orthogonalProjection s₁ p : P) ≠ orthogonalProjection s₂ p)
(hp₁ : haveI : Nonempty s₁ := ⟨p', hp'.1⟩; orthogonalProjection s₁ p ≠ p')
(hp₂ : haveI : Nonempty s₂ := ⟨p', hp'.2⟩; orthogonalProjection s₂ p ≠ p') :
haveI : Nonempty s₁ := ⟨p', hp'.1⟩
haveI : Nonempty s₂ := ⟨p', hp'.2⟩
dist p (orthogonalProjection s₁ p) = dist p (orthogonalProjection s₂ p) ↔
∡ (orthogonalProjection s₁ p : P) p' p = ∡ p p' (orthogonalProjection s₂ p) :=
```
that is an oriented angle analogue of the existing
`dist_orthogonalProjection_eq_iff_angle_eq`. Because the minimal
nondegeneracy conditions required for the two directions of this lemma
are different (whereas the unoriented version doesn't need any
nondegeneracy conditions), those two directions are added as separate
lemmas, each with minimal nondegeneracy conditions, from which the
`iff` version is then deduced.
…ality of twice angles
Add lemmas that two angles less than `π / 2` are equal if and only if
twice those angles are equal, along with a separate lemma
```lean
lemma toReal_neg_eq_neg_toReal_iff {θ : Angle} : (-θ).toReal = -(θ.toReal) ↔ θ ≠ π := by
```
which isn't directly connected but turns out to be useful in the same
application (dealing with angles in right-angled triangles that are
less then `π / 2`, when you have two such triangles that are
oppositely-oriented).
…`π / 2` Add a lemma that an oriented angle in a right-angled triangle is less than `π / 2`, even in degenerate cases (there's already a corresponding lemma for unoriented angles, but that one needs to exclude some degenerate cases because of the different default values for oriented and unoriented angles involving zero vectors). Deduce lemmas that, for such angles involved in right-angled triangles, equality of the angles (i.e. equality mod 2π) follows from equality of twice the angles (i.e. equality of the angles mod π).
Add a lemma
```lean
lemma orthogonalProjection_eq_iff_mem {s : AffineSubspace ℝ P} [Nonempty s]
[s.direction.HasOrthogonalProjection] {p q : P} :
orthogonalProjection s p = q ↔ q ∈ s ∧ p -ᵥ q ∈ s.directionᗮ := by
```
that gives the characteristic property of the orthogonal projection in
a more convenient form to use than the existing
`inter_eq_singleton_orthogonalProjection` (from which it is derived).
…ion_orthogonalProjection_of_le
…isector_dist_oangle
Add instances that the supremum of two affine subspaces, either one nonempty, is nonempty. These are useful when working with orthogonal projections onto such a supremum.
…ion_sup_of_orthogonalProjection_eq
Add a lemma that, if the orthogonal projections of a point onto two subspaces are equal, so is the projection onto their supremum.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…sup_of_orthogonalProjection_eq
…ion_orthogonalProjection_of_le
…isector_dist_oangle
…ion_sup_of_orthogonalProjection_eq
…ion_orthogonalProjection_of_le
…isector_dist_oangle
…ion_sup_of_orthogonalProjection_eq
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…ion_orthogonalProjection_of_le
…isector_dist_oangle
…ion_sup_of_orthogonalProjection_eq
mathlib-dependent-issues
Bot
removed
the
blocked-by-other-PR
wwylele
approved these changes
Mar 29, 2026
| lemma angle_incenter_eq_angle_div_two {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) | ||
| (h₂₃ : i₂ ≠ i₃) : | ||
| ∠ (t.points i₂) (t.points i₁) t.incenter = ∠ (t.points i₂) (t.points i₁) (t.points i₃) / 2 := by | ||
| let S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points) |
Collaborator
There was a problem hiding this comment.
Random idea and not in the scope of the PR: should we have a "planarize" tactic that handles restricting everything to the subspace?
Contributor
Author
There was a problem hiding this comment.
Something like that would be reasonable (once we have enough examples to show e.g. what's most convenient in terms of choosing the two-dimensional subspace / showing that all points lie in it / possibly dealing with any special cases where actually the ambient space is less than two-dimensional). Note that we don't yet have a full set of map / restrict lemmas for all simplex definitions, though that might only matter when they're missing for the particular definition you wish to transport to a two-dimensional subspace in a particular case.
Comment on lines
+302
to
+305
| have hf2 : Fact (finrank ℝ S.direction = 2) := ⟨by | ||
| simp_rw [S] | ||
| rw [direction_affineSpan, t.independent.finrank_vectorSpan] | ||
| simp⟩ |
Contributor
There was a problem hiding this comment.
you repeat this code block four times. Can this be some lemma?
Contributor
Author
There was a problem hiding this comment.
See #39696 - rather than making other PRs depend on it, I was assuming that as a straightforward PR that had been requested on Zulip, it would be reviewed quickly and then I could merge master into existing PRs and update them accordingly.
|
|
||
| set_option backward.isDefEq.respectTransparency false in | ||
| /-- The incenter of a triangle bisects the angle at a vertex. -/ | ||
| lemma angle_incenter_eq_angle_div_two {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) |
Contributor
There was a problem hiding this comment.
I wonder if it may be useful/convenient to have copies of these lemmas stating "2 *∠ (t.points i₂) (t.points i₁) t.incenter = ∠ (t.points i₂) (t.points i₁) (t.points i₃)"? (not sure)
Contributor
Author
There was a problem hiding this comment.
I'm not convinced that's sufficiently useful to be worth duplicating all these lemmas, when you can always substitute this version in if you need the other one. (Most of the time the oriented versions are more useful anyway; it simply happened I needed angle inequalities to prove configuration information, which meant I wanted an explicit expression for the angle involving the incenter.)
Contributor
|
awaiting-author |
github-actions
Bot
added
the
awaiting-author
Contributor
|
cool lemmas! |
Co-authored-by: Felix Pernegger <s59fpern@uni-bonn.de>
jsm28
removed
the
awaiting-author
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
7 participants
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.
Add lemmas giving unoriented angles involving the incenter and excenters of a triangle as expressions involving dividing angles of the triangle by 2, deduced from oriented bisection lemmas.
mapand subtype lemmas #32019mapandrestrictlemmas #32021toRealaddition lemmas #32259mapandrestrictlemmas #32270