dist_reflection_eq_of_mem — Mathlib

English

The distance between p1 and the reflection of p2 across s equals the distance between the reflection of p1 across s and p2.

Русский

Расстояние между p1 и отражением p2 через s равно расстоянию между отражением p1 через s и p2.

LaTeX

$$$$\operatorname{dist}(p_1, \mathrm{reflection}_s(p_2)) = \operatorname{dist}(\mathrm{reflection}_s(p_1), p_2).$$$$

Lean4

/-- A point in the subspace is equidistant from another point and its
reflection. -/
theorem dist_reflection_eq_of_mem (s : AffineSubspace ℝ P) [Nonempty s] [s.direction.HasOrthogonalProjection] {p₁ : P}
    (hp₁ : p₁ ∈ s) (p₂ : P) : dist p₁ (reflection s p₂) = dist p₁ p₂ :=
  by
  rw [← reflection_eq_self_iff p₁] at hp₁
  convert (reflection s).dist_map p₁ p₂
  rw [hp₁]

Похожие утверждения