mem_span_insert' — Mathlib

English

If i ≠ j, then span of the range of the function v updated at j by v(j) + r v(i) equals span of the original range of v.

Русский

Если i ≠ j, то оболочка множества значений функции v после обновления в позиции j на v(j) + r v(i) имеет тот же span, что и исходная

LaTeX

$$$\operatorname{span}_R\left(\operatorname{range}(\operatorname{Function.update}(v,j,v(j)+r\cdot v(i)))\right) = \operatorname{span}_R(\operatorname{range}(v))$$$

Lean4

theorem mem_span_insert' {x y} {s : Set M} : x ∈ span R (insert y s) ↔ ∃ a : R, x + a • y ∈ span R s :=
  by
  rw [mem_span_insert]; constructor
  · rintro ⟨a, z, hz, rfl⟩
    exact ⟨-a, by simp [hz, add_assoc]⟩
  · rintro ⟨a, h⟩
    exact ⟨-a, _, h, by simp [add_comm]⟩

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