English
Let v: ι → V be a family of vectors. If v is linearly independent on a set s, and the vector v(x) is not in the span of {v(s)}, then v is linearly independent on the extended set insert x s.
Русский
Пусть v: ι → V — семейство векторов. Если v линейно независимо на множества s и вектор v(x) не принадлежит span{v(s)}, то v линейно независимо на объединении s с x.
LaTeX
$$$\text{LinearIndepOn}_K(v,s) \to \text{(v x) } \notin \operatorname{span}_K(v''s) \Rightarrow \text{LinearIndepOn}_K(v,\operatorname{insert} x\,s)$$$
Lean4
protected theorem insert {s : Set ι} {x : ι} (hs : LinearIndepOn K v s) (hx : v x ∉ span K (v '' s)) :
LinearIndepOn K v (insert x s) := by
rw [← union_singleton]
have x0 : v x ≠ 0 := fun h => hx (h ▸ zero_mem _)
apply hs.union (LinearIndepOn.singleton _ x0)
rwa [image_singleton, disjoint_span_singleton' x0]
