Theorems · Theorem · functional analysis

Orientation.finOrthonormalBasis_orientation

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ} (hn : 0 < n)
  (h : Module.finrank ℝ E = n) (x : Orientation ℝ E (Fin n)),
  (Orientation.finOrthonormalBasis hn h x).toBasis.orientation = x

Orientation.finOrthonormalBasis gives a basis with the required orientation.

Defined in

Mathlib.Analysis.InnerProductSpace.Orientation

Cited by

4 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpace