abs_volumeForm_apply_of_orthonormal

English

Volume form is compatible with change of coordinates via a linear isometry: mapping E to F preserves volume form up to orientation.

Русский

Объемная форма сохраняется при переходе по линейной изометрии: отображение через изометрию сохраняет объемную форму в соответствии с ориентацией.

LaTeX

$$$$ (\mathrm{Orientation.map}_{n} \phi^{\text{toLinearEquiv}}\ o).volumeForm = o.volumeForm \circ \phi^{\text{symm}}. $$$$

Lean4

/-- The output of the volume form of an oriented real inner product space `E` when evaluated on an
orthonormal basis is ±1. -/
theorem abs_volumeForm_apply_of_orthonormal (v : OrthonormalBasis (Fin n) ℝ E) : |o.volumeForm v| = 1 := by
  simpa [o.volumeForm_robust' v v] using congr_arg abs v.toBasis.det_self

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