English
The volume form is anti-invariant under negating orientation tensor: the volume form of the negative orientation is the negative of the original.
Русский
Объемная форма противодействует обращению ориентации: объемная форма отрицательной ориентации равна минусу исходной объемной формы.
LaTeX
$$$$ (-o).volumeForm = - o.volumeForm. $$$$
Lean4
@[simp]
theorem volumeForm_neg_orientation : (-o).volumeForm = -o.volumeForm :=
by
rcases n with - | n
· refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_ <;> rintro rfl
· simp [volumeForm_zero_neg]
· simp [volumeForm_zero_neg]
let e : OrthonormalBasis (Fin n.succ) ℝ E := o.finOrthonormalBasis n.succ_pos Fact.out
have h₁ : e.toBasis.orientation = o := o.finOrthonormalBasis_orientation _ _
have h₂ : e.toBasis.orientation ≠ -o := by
symm
rw [e.toBasis.orientation_ne_iff_eq_neg, h₁]
rw [o.volumeForm_robust e h₁, (-o).volumeForm_robust_neg e h₂]
