English
If i ≠ j, then span of the range of 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 span_range_update_add_smul (hij : i ≠ j) (v : ι → M) (r : R) :
span R (Set.range (Function.update v j (v j + r • v i))) = span R (Set.range v) :=
by
refine le_antisymm ?_ ?_ <;> simp only [span_le, Set.range_subset_iff, SetLike.mem_coe] <;> intro k <;>
obtain rfl | hjk := eq_or_ne j k
· rw [update_self]
exact add_mem (subset_span ⟨j, rfl⟩) <| smul_mem _ _ <| subset_span ⟨i, rfl⟩
· exact subset_span ⟨k, (update_of_ne hjk.symm ..).symm⟩
· nth_rw 2 [← add_sub_cancel_right (v j) (r • v i)]
exact sub_mem (subset_span ⟨j, update_self ..⟩) (smul_mem _ _ (subset_span ⟨i, update_of_ne hij ..⟩))
· exact subset_span ⟨k, update_of_ne hjk.symm ..⟩
