finOrthonormalBasis — Mathlib

English

An orientation-based orthonormal basis exists on Fin n via finOrthonormalBasis.

Русский

Существет ортонормированный базис на Fin n через finOrthonormalBasis.

LaTeX

$$$(Orientation.finOrthonormalBasis hn h x)$$$

Lean4

/-- An orthonormal basis, indexed by `Fin n`, with the given orientation. -/
protected def finOrthonormalBasis (hn : 0 < n) (h : finrank ℝ E = n) (x : Orientation ℝ E (Fin n)) :
    OrthonormalBasis (Fin n) ℝ E := by
  haveI := Fin.pos_iff_nonempty.1 hn
  haveI : FiniteDimensional ℝ E := .of_finrank_pos <| h.symm ▸ hn
  exact ((@stdOrthonormalBasis _ _ _ _ _ this).reindex <| finCongr h).adjustToOrientation x

Похожие утверждения