submatrix_gram — Mathlib

English

If we take a subindex map f : m → n, then the submatrix (Gram 𝕜 v) with both indices f is equal to the Gram matrix of v ∘ f.

Русский

Если взять подиндексовую карту f: m → n, то подматрица (Gram 𝕜 v) по f равна граммовой матрице вектора v ∘ f.

LaTeX

$$$ (\text{gram } 𝕜 v).\text{submatrix } f f = \text{gram } 𝕜 (v \circ f) $$$

Lean4

theorem submatrix_gram (v : n → E) {m : Set n} (f : m → n) : (gram 𝕜 v).submatrix f f = gram 𝕜 (v ∘ f) :=
  rfl

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