finOrthonormalBasis_orientation — Mathlib

English

finOrthonormalBasis_orientation asserts that the orientation of finOrthonormalBasis equals x.

Русский

Суждение finOrthonormalBasis_orientation утверждает, что ориентация finOrthonormalBasis равна x.

LaTeX

$$$\text{Orientation}(\text{finOrthonormalBasis})(x) = x$$$

Lean4

/-- `Orientation.finOrthonormalBasis` gives a basis with the required orientation. -/
@[simp]
theorem finOrthonormalBasis_orientation (hn : 0 < n) (h : finrank ℝ E = n) (x : Orientation ℝ E (Fin n)) :
    (x.finOrthonormalBasis hn h).toBasis.orientation = x :=
  by
  haveI := Fin.pos_iff_nonempty.1 hn
  haveI : FiniteDimensional ℝ E := .of_finrank_pos <| h.symm ▸ hn
  exact ((@stdOrthonormalBasis _ _ _ _ _ this).reindex <| finCongr h).orientation_adjustToOrientation x

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