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₁) (hp'₂ : p' ∈ 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₁) (hp'₂ : p' ∈ 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₁) (hp'₂ : p' ∈ 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₁) (hp'₂ : p' ∈ 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.

theorem EuclideanGeometry.dist_orthogonalProjection_eq_of_two_zsmul_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₁) (hp'₂ : p' ∈ s₂) : ↑((orthogonalProjection s₁) p) ≠ p' → ↑((orthogonalProjection s₂) p) ≠ p' → 2 • oangle (↑((orthogonalProjection s₁) p)) p' p = 2 • 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 twice the oriented angles at a point p' in their intersection between p and its orthogonal projections onto the subspaces are equal.

theorem EuclideanGeometry.dist_orthogonalProjection_line_eq_of_two_zsmul_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₂ p₃ : P} (h₂ : p₁ ≠ p₂) (h₃ : p₁ ≠ p₃) (h : 2 • oangle p₂ p₁ p = 2 • oangle p p₁ p₃) : dist p ↑((orthogonalProjection (affineSpan ℝ {p₁, p₂})) p) = dist p ↑((orthogonalProjection (affineSpan ℝ {p₁, p₃})) p)

A point p is equidistant to two lines p₁ p₂ and p₁ p₃ if the oriented angles at p₁ are equal modulo π.

theorem EuclideanGeometry.two_zsmul_oangle_eq_of_dist_orthogonalProjection_line_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₂ p₃ : P} (ha : AffineIndependent ℝ ![p₁, p₂, p₃]) (h : dist p ↑((orthogonalProjection (affineSpan ℝ {p₁, p₂})) p) = dist p ↑((orthogonalProjection (affineSpan ℝ {p₁, p₃})) p)) : 2 • oangle p₂ p₁ p = 2 • oangle p p₁ p₃

If a point p is equidistant to two different lines p₁ p₂ and p₁ p₃, the oriented angles at p₁ are equal modulo π.

theorem EuclideanGeometry.dist_orthogonalProjection_line_eq_iff_two_zsmul_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₂ p₃ : P} (ha : AffineIndependent ℝ ![p₁, p₂, p₃]) : dist p ↑((orthogonalProjection (affineSpan ℝ {p₁, p₂})) p) = dist p ↑((orthogonalProjection (affineSpan ℝ {p₁, p₃})) p) ↔ 2 • oangle p₂ p₁ p = 2 • oangle p p₁ p₃

A point p is equidistant to two different lines p₁ p₂ and p₁ p₃ if and only if the oriented angles at p₁ are equal modulo π.