orientation_ne_iff_eq_neg — Mathlib

English

Two orientations are unequal if and only if one is the negation of the other; i.e., not equal iff negation equality.

Русский

Две ориентации не равны тогда и только тогда, когда одна является отрицанием другой.

LaTeX

$$$$ x \\neq e.{\\rm orientation} \\quad\\iff\\quad x = -e.{\\rm orientation} $$$$

Lean4

/-- Given a basis, an orientation equals the negation of that given by that basis if and only
if it does not equal that given by that basis. -/
theorem orientation_ne_iff_eq_neg (e : Basis ι R M) (x : Orientation R M ι) : x ≠ e.orientation ↔ x = -e.orientation :=
  ⟨fun h => (e.orientation_eq_or_eq_neg x).resolve_left h, fun h =>
    h.symm ▸ (Module.Ray.ne_neg_self e.orientation).symm⟩

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