ne_iff_eq_neg — Mathlib

English

Two orientations are equal or not depending on their relationship with negation; if equal, not equal to negation, etc.

Русский

Две ориентации равны или не равны в зависимости от их отношения к отрицанию.

LaTeX

$$$$ x_1 = x_2 \\lor x_1 = -x_2 $$$$

Lean4

/-- If the index type has cardinality equal to the finite dimension, an orientation equals the
negation of another orientation if and only if they are not equal. -/
theorem ne_iff_eq_neg [FiniteDimensional R M] (x₁ x₂ : Orientation R M ι) (h : Fintype.card ι = finrank R M) :
    x₁ ≠ x₂ ↔ x₁ = -x₂ :=
  ⟨fun hn => (eq_or_eq_neg x₁ x₂ h).resolve_left hn, fun he => he.symm ▸ (Module.Ray.ne_neg_self x₂).symm⟩

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