span_range_h_le_range_diagonal — Mathlib

English

The span of the matrices h(i) over i is contained in the range of the diagonal-linear map.

Русский

Образ всех h(i) расположен в образе диагонального линейного отображения.

LaTeX

$$span R (range h) ≤ range (Matrix.diagonalLinearMap (b.support ⊕ ι) R R)$$

Lean4

theorem span_range_h_le_range_diagonal [DecidableEq ι] :
    span R (range h) ≤ LinearMap.range (Matrix.diagonalLinearMap (b.support ⊕ ι) R R) :=
  by
  rw [span_le]
  rintro - ⟨i, rfl⟩
  rw [h_eq_diagonal]
  exact LinearMap.mem_range_self _ _

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