gramSchmidtOrthonormalBasis_inv_triangular'

English

A variant asserting the same vanishing inner products for the primed representation.

Русский

Вариант утверждения о нулевых скалярных произведениях для представления с пометкой 'прикрепления'.

LaTeX

$$$$ \langle (\mathrm{gramSchmidtOrthonormalBasis}(h,f))_j, f_i \rangle = 0 \quad \text{for } i

Lean4

theorem gramSchmidtOrthonormalBasis_inv_triangular' {i j : ι} (hij : i < j) :
    (gramSchmidtOrthonormalBasis h f).repr (f i) j = 0 := by
  simpa [OrthonormalBasis.repr_apply_apply] using gramSchmidtOrthonormalBasis_inv_triangular h f hij

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