orthonormal_adjustToOrientation — Mathlib

English

adjustToOrientation preserves orthonormality.

Русский

adjustToOrientation сохраняет ортонормированность.

LaTeX

$$$\text{Orthonormal Real } E$ after adjustment$$

Lean4

/-- `OrthonormalBasis.adjustToOrientation`, applied to an orthonormal basis, preserves the
property of orthonormality. -/
theorem orthonormal_adjustToOrientation : Orthonormal ℝ (e.toBasis.adjustToOrientation x) :=
  by
  apply e.orthonormal.orthonormal_of_forall_eq_or_eq_neg
  simpa using e.toBasis.adjustToOrientation_apply_eq_or_eq_neg x

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