reflection_orthogonal — Mathlib

English

Let K be a subspace of an inner product space with an orthogonal projection. The reflection across the orthogonal complement K⊥ equals the reflection across K composed with negation.

Русский

Пусть K — подпространство эллиптического пространства с ортогональной проекцией. Отражение по ортогональному дополнению K⊥ совпадает с отражением по K, затем с отрицанием.

LaTeX

$$$R_{K^{\perp}} = R_K \circ (-\mathrm{id}_E)$$$

Lean4

theorem reflection_orthogonal : Kᗮ.reflection = .trans K.reflection (.neg _) := by ext;
  apply reflection_orthogonal_apply

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