adjustToOrientation_apply_eq_or_eq_neg

English

Each vector in e.adjustToOrientation(x) is either the same as in e or its negation.

Русский

Каждый вектор e.adjustToOrientation(x) либо равен соответствующему вектору e, либо его противоположности.

LaTeX

$$$\forall i,\ e.adjustToOrientation(x)_i = e_i \,\lor\ e.adjustToOrientation(x)_i = -e_i$$$

Lean4

/-- Every basis vector from `adjustToOrientation` is either that from the original basis or its
negation. -/
theorem adjustToOrientation_apply_eq_or_eq_neg (i : ι) :
    e.adjustToOrientation x i = e i ∨ e.adjustToOrientation x i = -e i := by
  simpa [← e.toBasis_adjustToOrientation] using e.toBasis.adjustToOrientation_apply_eq_or_eq_neg x i

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