English
If v is LI on s and t with disjoint spans, then v is LI on s ∪ t.
Русский
Если v линейно независимо на s и t, причём их линейные оболочки не пересекаются, то v линейно независимо на объединение s и t.
LaTeX
$$$\\text{LinearIndepOn } R\\ v\\ s \\to \\text{LinearIndepOn } R\\ v\\ t \\to \\text{Disjoint}(\\operatorname{span}R(\\operatorname{image}(v,s)), \\operatorname{span}R(\\operatorname{image}(v,t))) \\to \\text{LinearIndepOn } R\\ v (s\\cup t)$$$
Lean4
theorem union {t : Set ι} (hs : LinearIndepOn R v s) (ht : LinearIndepOn R v t)
(hdj : Disjoint (span R (v '' s)) (span R (v '' t))) : LinearIndepOn R v (s ∪ t) :=
by
nontriviality R
classical
have hli := LinearIndependent.sum_type hs ht (by rwa [← image_eq_range, ← image_eq_range])
have hdj := (hdj.of_span₀ hs.zero_notMem_image).of_image
rw [LinearIndepOn]
convert (hli.comp _ (Equiv.Set.union hdj).injective) with ⟨x, hx | hx⟩
· rw [comp_apply, Equiv.Set.union_apply_left _ hx, Sum.elim_inl]
rw [comp_apply, Equiv.Set.union_apply_right _ hx, Sum.elim_inr]
