reflection_apply_left — Mathlib

English

If i and j are orthogonal, then applying reflection j to the root i fixes it: P.reflection j (P.root i) = P.root i.

Русский

Если i и j ортогональны, то применение отражения j к корню i оставляет его неизменным.

LaTeX

$$$$ P.reflection_j( P.root_i ) = P.root_i. $$$$

Lean4

theorem reflection_apply_left (h : IsOrthogonal P i j) : P.reflection j (P.root i) = P.root i := by
  simp [reflection_apply, h.1]

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