adjustToOrientation — Mathlib

English

orientation of adjusted basis equals x.

Русский

ориентация приведённого базиса равна x.

LaTeX

$$$(e.adjustToOrientation x).toBasis.orientation = x$$$

Lean4

/-- Given an orthonormal basis and an orientation, return an orthonormal basis giving that
orientation: either the original basis, or one constructed by negating a single (arbitrary) basis
vector. -/
def adjustToOrientation : OrthonormalBasis ι ℝ E :=
  (e.toBasis.adjustToOrientation x).toOrthonormalBasis (e.orthonormal_adjustToOrientation x)

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