Theorems · Theorem · geometry

EuclideanGeometry.dist_orthogonalProjection_eq_iff_angle_eq

∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p p' : P} {s₁ s₂ : AffineSubspace ℝ P} [inst_4 : s₁.direction.HasOrthogonalProjection]
  [inst_5 : s₂.direction.HasOrthogonalProjection] (hp'₁ : p' ∈ s₁) (hp'₂ : p' ∈ s₂),
  dist p ↑((EuclideanGeometry.orthogonalProjection s₁) p) = dist p ↑((EuclideanGeometry.orthogonalProjection s₂) p) ↔
    EuclideanGeometry.angle p p' ↑((EuclideanGeometry.orthogonalProjection s₁) p) =
      EuclideanGeometry.angle p p' ↑((EuclideanGeometry.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.

Defined in

Mathlib.Geometry.Euclidean.Angle.Bisector

Cited by

4 results in Mathlib

Foundations

Depth 204 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsorSubmodule.HasOrthogonalProjectionSubmodule.HasOrthogonalProjection