Theorems · Definition · functional analysis

OrthonormalBasis.adjustToOrientation

{E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] →
      {ι : Type u_2} →
        [inst_2 : Fintype ι] →
          [DecidableEq ι] → OrthonormalBasis ι ℝ E → Orientation ℝ E ι → [Nonempty ι] → OrthonormalBasis ι ℝ E

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.

Defined in

Mathlib.Analysis.InnerProductSpace.Orientation

Cited by

7 results in Mathlib

Foundations

Depth 231 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceFintypeDecidableEqNonempty