Commit 2025-11-14 20:02 48bd45eb

feat(Geometry/Euclidean/Angle/Bisector): oriented angle bisection and equal distance (#30477) Add a lemma

lemma dist_orthogonalProjection_eq_iff_oangle_eq {p p' : P} {s₁ s₂ : AffineSubspace ℝ P}
    (hp' : p' ∈ s₁ ⊓ s₂) :
    haveI : Nonempty s₁ := ⟨p', hp'.1⟩
    haveI : Nonempty s₂ := ⟨p', hp'.2⟩
    (orthogonalProjection s₁ p : P) ≠ orthogonalProjection s₂ p →
    orthogonalProjection s₁ p ≠ p' →
    orthogonalProjection s₂ p ≠ p' →
    (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.