English
Let R be a semiring and v a family of vectors v: ι → M in an R-module M. If {s_i} is a directed family of subsets of ι (ordered by inclusion) and each restriction of v to s_i is linearly independent, then the union of all s_i yields a linearly independent family on v.
Русский
Пусть R – полукольцо и пусть v: ι → M — семейство векторов в модуле над R. Если {s_i} — направленная по включению система подмножеств ι и ограничение v на каждое s_i линейно независимо, то объединение всех s_i также даёт линейно независимое множество на v.
LaTeX
$$$\\bigl(\\forall i,\\ LinearIndepOn_R(v, s_i)\\bigr) \\Rightarrow \\ LinearIndepOn_R(v, \\bigcup_i s_i)$$
Lean4
theorem linearIndepOn_iUnion_of_directed {η : Type*} {s : η → Set ι} (hs : Directed (· ⊆ ·) s)
(h : ∀ i, LinearIndepOn R v (s i)) : LinearIndepOn R v (⋃ i, s i) :=
by
by_cases hη : Nonempty η
· refine linearIndepOn_of_finite (⋃ i, s i) fun t ht ft => ?_
rcases finite_subset_iUnion ft ht with ⟨I, fi, hI⟩
rcases hs.finset_le fi.toFinset with ⟨i, hi⟩
exact (h i).mono (Subset.trans hI <| iUnion₂_subset fun j hj => hi j (fi.mem_toFinset.2 hj))
· refine (linearIndepOn_empty R v).mono (t := iUnion (s ·)) ?_
rintro _ ⟨_, ⟨i, _⟩, _⟩
exact hη ⟨i⟩
