English
Under LinearIndepOn K id s, not having a ∈ span_K s is equivalent to the independence on insert a s together with a not in s.
Русский
Если LinearIndepOn K id s, то не принадлежность a порождению span_K s эквивалентна независимости на insert a s и тому, что a ∉ s.
LaTeX
$$$\text{LinearIndepOn}_K(\text{id},s) \Rightarrow \Bigl( a \notin \operatorname{span}_K(s) \Rightarrow \text{LinearIndepOn}_K(\text{id},\operatorname{insert} a\,s) \Bigr)$$$
Lean4
theorem linearIndepOn_insert {s : Set ι} {a : ι} {f : ι → V} (has : a ∉ s) :
LinearIndepOn K f (insert a s) ↔ LinearIndepOn K f s ∧ f a ∉ Submodule.span K (f '' s) := by
classical
rw [LinearIndepOn, LinearIndepOn, ←
linearIndependent_equiv ((Equiv.optionEquivSumPUnit _).trans (Equiv.Set.insert has).symm), linearIndependent_option]
simp only [comp_def]
rw [range_comp']
simp
