reflection_eq_self_iff — Mathlib

English

For any x in E, reflecting across K fixes x if and only if x lies in K.

Русский

Отражение в K фиксирует вектор x тогда и только тогда, когда x принадлежит K.

LaTeX

$$$R_K(x) = x \iff x \in K$$$

Lean4

/-- A point is its own reflection if and only if it is in the subspace. -/
theorem reflection_eq_self_iff (x : E) : K.reflection x = x ↔ x ∈ K :=
  by
  rw [← starProjection_eq_self_iff, reflection_apply, sub_eq_iff_eq_add', ← two_smul 𝕜, two_smul ℕ, ← two_smul 𝕜]
  refine (smul_right_injective E ?_).eq_iff
  exact two_ne_zero

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