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_basisis an orthonormal basis, indexed byfin n, with the given orientation.
theorem
orthonormal.orthonormal_adjust_to_orientation
{E : Type u_1}
[inner_product_space ℝ E]
{ι : Type u_2}
[fintype ι]
[decidable_eq ι]
[nonempty ι]
{e : basis ι ℝ E}
(h : orthonormal ℝ ⇑e)
(x : orientation ℝ E ι) :
basis.adjust_to_orientation, applied to an orthonormal basis, produces an orthonormal
basis.
@[protected]
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.
Equations
@[protected]
theorem
orientation.fin_orthonormal_basis_orthonormal
{E : Type u_1}
[inner_product_space ℝ E]
{n : ℕ}
(hn : 0 < n)
(h : finite_dimensional.finrank ℝ E = n)
(x : orientation ℝ E (fin n)) :
orientation.fin_orthonormal_basis is orthonormal.
@[simp]
theorem
orientation.fin_orthonormal_basis_orientation
{E : Type u_1}
[inner_product_space ℝ E]
{n : ℕ}
(hn : 0 < n)
(h : finite_dimensional.finrank ℝ E = n)
(x : orientation ℝ E (fin n)) :
(orientation.fin_orthonormal_basis hn h x).orientation = x
orientation.fin_orthonormal_basis gives a basis with the required orientation.