English
If the orientation is negated, the volume form changes sign accordingly: the volume form of the negated orientation is the negative of the original volume form.
Русский
При обращении ориентации знак объемной формы меняется: объемная форматорованной ориентированности равна минус исходной объемной формы.
LaTeX
$$$$ (-o).volumeForm = -\, o.volumeForm. $$$$
Lean4
theorem volumeForm_zero_neg [_i : Fact (finrank ℝ E = 0)] :
Orientation.volumeForm (-positiveOrientation : Orientation ℝ E (Fin 0)) =
-AlternatingMap.constLinearEquivOfIsEmpty 1 :=
by
simp_rw [volumeForm, Or.by_cases, positiveOrientation]
apply if_neg
simp only [neg_rayOfNeZero]
rw [ray_eq_iff, SameRay.sameRay_comm]
intro h
simpa using congr_arg AlternatingMap.constLinearEquivOfIsEmpty.symm (eq_zero_of_sameRay_self_neg h)
