orientation_adjustToOrientation — Mathlib

English

The Fin-n indexed orthonormal basis has orientation equal to x.

Русский

Ортонормированный базис с индексацией Fin имеет ориентацию x.

LaTeX

$$$((x.finOrthonormalBasis\ hn h).toBasis.orientation = x)$$$

Lean4

/-- `adjustToOrientation` gives an orthonormal basis with the required orientation. -/
@[simp]
theorem orientation_adjustToOrientation : (e.adjustToOrientation x).toBasis.orientation = x :=
  by
  rw [e.toBasis_adjustToOrientation]
  exact e.toBasis.orientation_adjustToOrientation x

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