English
The orientation determined by a basis equals any orientation or its negation; i.e., every orientation is either equal to the basis orientation or its negation.
Русский
Ориентация, заданная базисом, равна самой ориентации базиса или её отрицанию; любая ориентация равна ориентации базиса или её отрицанию.
LaTeX
$$$$ x = e.{\\rm orientation} \\;\\lor\\; x = -e.{\\rm orientation} $$$$
Lean4
/-- Given a basis, any orientation equals the orientation given by that basis or its negation. -/
theorem orientation_eq_or_eq_neg (e : Basis ι R M) (x : Orientation R M ι) : x = e.orientation ∨ x = -e.orientation :=
by
induction x using Module.Ray.ind with
| h x hx =>
rw [← x.map_basis_ne_zero_iff e] at hx
rwa [Basis.orientation, ray_eq_iff, neg_rayOfNeZero, ray_eq_iff, x.eq_smul_basis_det e,
sameRay_neg_smul_left_iff_of_ne e.det_ne_zero hx, sameRay_smul_left_iff_of_ne e.det_ne_zero hx, lt_or_lt_iff_ne,
ne_comm]
