adjustToOrientation_apply_eq_or_eq_neg

English

Each vector of the adjusted basis is either the corresponding vector of the original basis or its negation.

Русский

Каждый вектор в откорректированном базисе равен соответствующему вектору исходного базиса или его отрицанию.

LaTeX

$$$$ e.{\\rm adjustToOrientation} x\, i = e\,i \\,\\lor\\, e.{\\rm adjustToOrientation} x\, i = -e\,i $$$$

Lean4

/-- Every basis vector from `adjust_to_orientation` is either that from the original basis or its
negation. -/
theorem adjustToOrientation_apply_eq_or_eq_neg [Nonempty ι] (e : Basis ι R M) (x : Orientation R M ι) (i : ι) :
    e.adjustToOrientation x i = e i ∨ e.adjustToOrientation x i = -e i :=
  by
  rw [adjustToOrientation]
  split_ifs with h
  · simp
  · by_cases hi : i = Classical.arbitrary ι <;> simp [unitsSMul_apply, hi]

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