English
Let p be a point and p′ lie in the intersection s1 ∩ s2 of two affine subspaces for which orthogonal projections onto their directions exist. Then the distance from p to the projection onto s1 equals the distance to the projection onto s2 if and only if the angle at p′ between p and its projections onto s1 and s2 are equal.
Русский
Пусть p — точка, а p′ лежит в пересечении двух аффинных подпомещений; допускается существование ортогональных проекций на направления подполь. Тогда расстояние от p до проекции на s1 равно расстоянию до проекции на s2 тогда и только тогда, когда угол в p′ между p и его проекциям на s1 и s2 равен.
LaTeX
$$$\\dist p (orthogonalProjection(s_1, p)) = dist p (orthogonalProjection(s_2, p)) \\iff \\\\ ∠ p p' (orthogonalProjection(s_1, p)) = ∠ p p' (orthogonalProjection(s_2, p))$$$
Lean4
/-- 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 dist_orthogonalProjection_eq_iff_angle_eq {p p' : P} {s₁ s₂ : AffineSubspace ℝ P}
[s₁.direction.HasOrthogonalProjection] [s₂.direction.HasOrthogonalProjection] (hp' : p' ∈ s₁ ⊓ s₂) :
haveI : Nonempty s₁ := ⟨p', hp'.1⟩
haveI : Nonempty s₂ := ⟨p', hp'.2⟩
dist p (orthogonalProjection s₁ p) = dist p (orthogonalProjection s₂ p) ↔
∠ p p' (orthogonalProjection s₁ p) = ∠ p p' (orthogonalProjection s₂ p) :=
by
have : Nonempty s₁ := ⟨p', hp'.1⟩
have : Nonempty s₂ := ⟨p', hp'.2⟩
by_cases h' : p ∈ s₁ ∨ p ∈ s₂
· exact dist_orthogonalProjection_eq_iff_angle_eq_aux hp' h'
rw [not_or] at h'
rw [angle_comm,
angle_eq_arcsin_of_angle_eq_pi_div_two ?_ (.inl (Ne.symm (orthogonalProjection_eq_self_iff.symm.not.1 h'.1))),
angle_comm,
angle_eq_arcsin_of_angle_eq_pi_div_two ?_ (.inl (Ne.symm (orthogonalProjection_eq_self_iff.symm.not.1 h'.2)))]
· refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
· rw [h]
· have hp : p ≠ p' := by
rintro rfl
exact h'.1 hp'.1
have hpd : 0 < dist p p' := dist_pos.2 hp
rw [Real.arcsin_inj (le_trans (by norm_num : (-1 : ℝ) ≤ 0) (by positivity)) ((div_le_one hpd).2 ?_)
(le_trans (by norm_num : (-1 : ℝ) ≤ 0) (by positivity)) ((div_le_one hpd).2 ?_)] at h
· rwa [div_left_inj' hpd.ne'] at h
· rw [dist_orthogonalProjection_eq_infDist]
exact Metric.infDist_le_dist_of_mem (SetLike.mem_coe.1 hp'.1)
· rw [dist_orthogonalProjection_eq_infDist]
exact Metric.infDist_le_dist_of_mem (SetLike.mem_coe.1 hp'.2)
· rw [angle, ← InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two]
exact
Submodule.inner_left_of_mem_orthogonal (K := s₂.direction)
(AffineSubspace.vsub_mem_direction hp'.2 (orthogonalProjection_mem _))
(vsub_orthogonalProjection_mem_direction_orthogonal _ _)
· rw [angle, ← InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two]
exact
Submodule.inner_left_of_mem_orthogonal (K := s₁.direction)
(AffineSubspace.vsub_mem_direction hp'.1 (orthogonalProjection_mem _))
(vsub_orthogonalProjection_mem_direction_orthogonal _ _)
