dist_reflection — Mathlib

English

If p1 lies in s, then the distance from p1 to the reflection of p2 equals the distance from p1 to p2.

Русский

Если p1 лежит в s, то dist(p1, refl_s(p2)) = dist(p1, p2).

LaTeX

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

Lean4

/-- The distance between `p₁` and the reflection of `p₂` equals that
between the reflection of `p₁` and `p₂`. -/
theorem dist_reflection (s : AffineSubspace ℝ P) [Nonempty s] [s.direction.HasOrthogonalProjection] (p₁ p₂ : P) :
    dist p₁ (reflection s p₂) = dist (reflection s p₁) p₂ :=
  by
  conv_lhs => rw [← reflection_reflection s p₁]
  exact (reflection s).dist_map _ _

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