English
For nonzero x ∈ E, the pair (x, J x) forms a basis of E (i.e., spans E and is linearly independent).
Русский
Для не нулевого вектора x ∈ E пара (x, J x) образует базис пространства E.
LaTeX
$$$\\text{span}_{\\\\mathbb{R}}\\{x, J x\\} = E \\quad\\text{и}\\quad x, J x \\text{ линейно независимы}$$$
Lean4
/-- For a nonzero vector `x` in an oriented two-dimensional real inner product space `E`,
`![x, J x]` forms an (orthogonal) basis for `E`. -/
def basisRightAngleRotation (x : E) (hx : x ≠ 0) : Basis (Fin 2) ℝ E :=
@basisOfLinearIndependentOfCardEqFinrank ℝ _ _ _ _ _ _ _ ![x, J x]
(linearIndependent_of_ne_zero_of_inner_eq_zero (fun i => by fin_cases i <;> simp [hx])
(by
intro i j hij
fin_cases i <;> fin_cases j <;> simp_all))
(@Fact.out (finrank ℝ E = 2)).symm