reflection_eq_self_iff — Mathlib

English

A point p is fixed by reflection across s exactly when p lies in s.

Русский

Точка фиксируется отражением через s тогда и только тогда, когда она лежит в s.

LaTeX

$$$$\mathrm{reflection}_s(p) = p \iff p \in s.$$$$

Lean4

/-- A point is its own reflection if and only if it is in the subspace. -/
theorem reflection_eq_self_iff {s : AffineSubspace ℝ P} [Nonempty s] [s.direction.HasOrthogonalProjection] (p : P) :
    reflection s p = p ↔ p ∈ s :=
  by
  rw [← orthogonalProjection_eq_self_iff, reflection_apply]
  constructor
  · intro h
    rw [← @vsub_eq_zero_iff_eq V, vadd_vsub_assoc, ← two_smul ℝ (↑(orthogonalProjection s p) -ᵥ p), smul_eq_zero] at h
    norm_num at h
    exact h
  · intro h
    simp [h]

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