E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
⊢ ∀ (i : ι),
    ↑(Basis.adjustToOrientation (OrthonormalBasis.toBasis e) x) i = ↑e i ∨
      ↑(Basis.adjustToOrientation (OrthonormalBasis.toBasis e) x) i = -↑e i
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
⊢ Orthonormal ℝ ↑(Basis.adjustToOrientation (OrthonormalBasis.toBasis e) x)
apply e.orthonormal.orthonormal_of_forall_eq_or_eq_neg
no goals
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
⊢ ∀ (i : ι),
    ↑(Basis.adjustToOrientation (OrthonormalBasis.toBasis e) x) i = ↑e i ∨
      ↑(Basis.adjustToOrientation (OrthonormalBasis.toBasis e) x) i = -↑e i
simpa using e.toBasis.adjustToOrientation_apply_eq_or_eq_neg x