reflection_mem_subspace_orthogonal_precomplement_eq_neg

English

If v ∈ K, then reflection in K⊥ equals negation of v when considered in the orthogonal complement context.

Русский

Если v ∈ K, то отражение в K⊥ даёт −v (в смысле элемента K).

LaTeX

$$$v \in K \Rightarrow R_{K^{\perp}}(v) = -v$$$

Lean4

/-- The reflection in `Kᗮ` of an element of `K` is its negation. -/
theorem reflection_mem_subspace_orthogonal_precomplement_eq_neg {v : E} (hv : v ∈ K) : Kᗮ.reflection v = -v :=
  reflection_mem_subspace_orthogonalComplement_eq_neg (K.le_orthogonal_orthogonal hv)

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