span_apply — Mathlib

English

If i belongs to the finite index set s, then the i-th basis vector of the span equals v'(i).

Русский

Если i принадлежит множеству индексов s, то i-й вектор базиса в подпространстве, образованном span, равен v'(i).

LaTeX

$$$$ \\text{If } i \\in s, \\quad (\\mathrm{OrthonormalBasis.span}(h,s))(i) = v'(i). $$$$

Lean4

@[simp]
protected theorem span_apply [DecidableEq E] {v' : ι' → E} (h : Orthonormal 𝕜 v') (s : Finset ι') (i : s) :
    (OrthonormalBasis.span h s i : E) = v' i := by
  simp only [OrthonormalBasis.span, Basis.span_apply, LinearIsometryEquiv.ofEq_symm, OrthonormalBasis.map_apply,
    OrthonormalBasis.coe_mk, LinearIsometryEquiv.coe_ofEq_apply, comp_apply]

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