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.