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