# mathlibdocumentation

analysis.inner_product_space.orientation

# Orientations of real inner product spaces. #

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

## Main definitions #

• orientation.fin_orthonormal_basis is an orthonormal basis, indexed by fin n, with the given orientation.
theorem orthonormal_basis.orthonormal_adjust_to_orientation {E : Type u_1} {ι : Type u_2} [fintype ι] [decidable_eq ι] [nonempty ι] (e : E) (x : ι) :

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} {ι : Type u_2} [fintype ι] [decidable_eq ι] [nonempty ι] (e : E) (x : ι) :

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.

Equations
theorem orthonormal_basis.to_basis_adjust_to_orientation {E : Type u_1} {ι : Type u_2} [fintype ι] [decidable_eq ι] [nonempty ι] (e : E) (x : ι) :
@[simp]
theorem orthonormal_basis.orientation_adjust_to_orientation {E : Type u_1} {ι : Type u_2} [fintype ι] [decidable_eq ι] [nonempty ι] (e : E) (x : ι) :

adjust_to_orientation gives an orthonormal basis with the required orientation.

theorem orthonormal_basis.adjust_to_orientation_apply_eq_or_eq_neg {E : Type u_1} {ι : Type u_2} [fintype ι] [decidable_eq ι] [nonempty ι] (e : E) (x : ι) (i : ι) :
i = e i i = -e i

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

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

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

Equations
@[simp]
theorem orientation.fin_orthonormal_basis_orientation {E : Type u_1} {n : } (hn : 0 < n) (h : = n) (x : (fin n)) :

orientation.fin_orthonormal_basis gives a basis with the required orientation.