fromOrthogonalSpanSingleton — Mathlib

English

The indexing map for the subordinate basis is defined in terms of the projection from the wrapped internal direct-sum structure.

Русский

Индексация подчинённой базы задаётся через проекцию оболочки внутреннего разложения на прямую сумму.

LaTeX

$$$\text{subordinateOrthonormalBasisIndex_def}$$$

Lean4

/-- Given a natural number `n` one less than the `finrank` of a finite-dimensional inner product
space, there exists an isometry from the orthogonal complement of a nonzero singleton to
`EuclideanSpace 𝕜 (Fin n)`. -/
def fromOrthogonalSpanSingleton (n : ℕ) [Fact (finrank 𝕜 E = n + 1)] {v : E} (hv : v ≠ 0) :
    OrthonormalBasis (Fin n) 𝕜 (𝕜 ∙ v)ᗮ :=
  have : FiniteDimensional 𝕜 E := .of_fact_finrank_eq_succ (K := 𝕜) (V := E) n
  (stdOrthonormalBasis _ _).reindex <| finCongr <| finrank_orthogonal_span_singleton hv

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