coe_mk — Mathlib

English

The underlying vector-valued function of the constructed orthonormal basis is exactly the original indexing function v. In particular, the basis produced by mk has as its i-th vector the original v(i).

Русский

Пусть v — зафиксированная система векторов; тогда базис, полученный посредством mk hon hsp, имеет вектор i-го индекса равным оригинальному v(i).

LaTeX

$$$$ (\\mathrm{OrthonormalBasis.mk}(hon,hsp))\\; =\\; v \\quad\\text{as functions} $$$$

Lean4

@[simp]
protected theorem coe_mk (hon : Orthonormal 𝕜 v) (hsp : ⊤ ≤ Submodule.span 𝕜 (Set.range v)) :
    ⇑(OrthonormalBasis.mk hon hsp) = v := by
  classical rw [OrthonormalBasis.mk, _root_.Module.Basis.coe_toOrthonormalBasis, Basis.coe_mk]

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