English
For any s,t, Disjoint s t, LinearIndepOn R f (s ∪ t) holds iff LinearIndepOn R f s and LinearIndepOn R (mkQ (span R (Set.image f s)).mkQ) t hold.
Русский
Для любых s,t, непересекающихся, LinearIndepOn R f (s ∪ t) эквивалентно LinearIndepOn R f s и LinearIndepOn R (mkQ (span R (Set.image f s)).mkQ) t.
LaTeX
$$$\text{LinearIndepOn}_R f (s \cup t) \iff \text{LinearIndepOn}_R f s \land \text{LinearIndepOn}_R (\text{Function.comp} (\mathrm{mkQ} (\mathrm{span}_R (\mathrm{Set.image} f s))). f) t$$$
Lean4
theorem linearIndepOn_union_iff_quotient {s t : Set ι} {f : ι → M} (hst : Disjoint s t) :
LinearIndepOn R f (s ∪ t) ↔ LinearIndepOn R f s ∧ LinearIndepOn R (mkQ (span R (f '' s)) ∘ f) t :=
by
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ h.1.union_of_quotient h.2⟩
· exact h.mono subset_union_left
apply (h.mono subset_union_right).map
simpa [← image_eq_range] using ((linearIndepOn_union_iff hst).1 h).2.2.symm
