orientation_adjustToOrientation — Mathlib

English

Adjusting a basis to match a given orientation yields a basis whose orientation exactly equals that target orientation.

Русский

Корректировка базиса до заданной ориентации даёт базис с именно этой ориентацией.

LaTeX

$$$$ (e.{\\rm adjustToOrientation} x).{\\rm orientation} = x $$$$

Lean4

/-- `adjust_to_orientation` gives a basis with the required orientation. -/
@[simp]
theorem orientation_adjustToOrientation [Nonempty ι] (e : Basis ι R M) (x : Orientation R M ι) :
    (e.adjustToOrientation x).orientation = x :=
  by
  rw [adjustToOrientation]
  split_ifs with h
  · exact h
  · rw [orientation_neg_single, eq_comm, ← orientation_ne_iff_eq_neg, ne_comm]
    exact h

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