mathlib documentation


Orientations of real inner product spaces. #

This file provides definitions and proves lemmas about orientations of real inner product spaces.

Main definitions #

orthonormal_basis.adjust_to_orientation, applied to an orthonormal basis, produces an orthonormal basis.

noncomputable def orthonormal_basis.adjust_to_orientation {E : Type u_1} [inner_product_space E] {ι : Type u_2} [fintype ι] [decidable_eq ι] [nonempty ι] (e : orthonormal_basis ι E) (x : orientation 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.


adjust_to_orientation gives an orthonormal basis with the required orientation.

Every basis vector from adjust_to_orientation is either that from the original basis or its negation.

noncomputable def orientation.fin_orthonormal_basis {E : Type u_1} [inner_product_space E] {n : } (hn : 0 < n) (h : finite_dimensional.finrank E = n) (x : orientation E (fin n)) :

An orthonormal basis, indexed by fin n, with the given orientation.


orientation.fin_orthonormal_basis gives a basis with the required orientation.