English
If s and t are disjoint, LI on v on s∪t is equivalent to LI on s and t and disjoint spans.
Русский
Если s и t дизjoint, LI на v на s∪t эквивалентно LI на s и t и раздельности их спанов.
LaTeX
$$$\\text{LinearIndepOn } R\\ v (s\\cup t) \\iff \\text{LinearIndepOn } R\\ v s \\land \\text{LinearIndepOn } R\\ v t \\land \\text{Disjoint}(\\operatorname{span}R s, \\operatorname{span}R t)$$$
Lean4
theorem linearIndepOn_union_iff {t : Set ι} (hdj : Disjoint s t) :
LinearIndepOn R v (s ∪ t) ↔
LinearIndepOn R v s ∧ LinearIndepOn R v t ∧ Disjoint (span R (v '' s)) (span R (v '' t)) :=
by
refine ⟨fun h ↦ ⟨h.mono subset_union_left, h.mono subset_union_right, ?_⟩, fun h ↦ h.1.union h.2.1 h.2.2⟩
convert h.disjoint_span_image (s := (↑) ⁻¹' s) (t := (↑) ⁻¹' t) (hdj.preimage _) <;> aesop
