Angle bisectors.

This file proves lemmas relating to bisecting angles.

theorem EuclideanGeometry.dist_orthogonalProjection_eq_iff_angle_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p p' : P} {s₁ s₂ : AffineSubspace ℝ P} [s₁.direction.HasOrthogonalProjection] [s₂.direction.HasOrthogonalProjection] (hp' : p' ∈ s₁ ⊓ s₂) : dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p) ↔ angle p p' ↑((orthogonalProjection s₁) p) = angle p p' ↑((orthogonalProjection s₂) p)

A point p is equidistant to two affine subspaces if and only if the angles at a point p' in their intersection between p and its orthogonal projections onto the subspaces are equal.

theorem EuclideanGeometry.dist_orthogonalProjection_eq_of_oangle_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p p' : P} {s₁ s₂ : AffineSubspace ℝ P} (hp' : p' ∈ s₁ ⊓ s₂) : ↑((orthogonalProjection s₁) p) ≠ p' → ↑((orthogonalProjection s₂) p) ≠ p' → oangle (↑((orthogonalProjection s₁) p)) p' p = oangle p p' ↑((orthogonalProjection s₂) p) → dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p)

A point p is equidistant to two affine subspaces (typically lines, for this version of the lemma) if the oriented angles at a point p' in their intersection between p and its orthogonal projections onto the subspaces are equal.

theorem EuclideanGeometry.oangle_eq_of_dist_orthogonalProjection_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p p' : P} {s₁ s₂ : AffineSubspace ℝ P} (hp' : p' ∈ s₁ ⊓ s₂) : ↑((orthogonalProjection s₁) p) ≠ ↑((orthogonalProjection s₂) p) → dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p) → oangle (↑((orthogonalProjection s₁) p)) p' p = oangle p p' ↑((orthogonalProjection s₂) p)

The oriented angles at a point p' in their intersection between p and its orthogonal projections onto two affine subspaces (typically lines, for this version of the lemma) are equal if p is equidistant to the two subspaces.

theorem EuclideanGeometry.dist_orthogonalProjection_eq_iff_oangle_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p p' : P} {s₁ s₂ : AffineSubspace ℝ P} (hp' : p' ∈ s₁ ⊓ s₂) : ↑((orthogonalProjection s₁) p) ≠ ↑((orthogonalProjection s₂) p) → ↑((orthogonalProjection s₁) p) ≠ p' → ↑((orthogonalProjection s₂) p) ≠ p' → (dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p) ↔ oangle (↑((orthogonalProjection s₁) p)) p' p = oangle p p' ↑((orthogonalProjection s₂) p))

A point p is equidistant to two affine subspaces (typically lines, for this version of the lemma) if and only if the oriented angles at a point p' in their intersection between p and its orthogonal projections onto the subspaces are equal.