English
If a directed family of subsets s_i of A has algebraic independence on each s_i, then the union ⋃ s_i is algebraically independent.
Русский
Если семейство направленных подмножеств s_i ⊆ A обладает алгебраической независимостью на каждом s_i, то объединение ⋃ s_i алгебраически независимо.
LaTeX
$$$\text{AlgebraicIndependent}_R (\bigcup_i s_i) \text{ given directedOn structure and each } s_i \text{ independent}$$$
Lean4
theorem algebraicIndependent_iUnion_of_directed {η : Type*} [Nonempty η] {s : η → Set A} (hs : Directed (· ⊆ ·) s)
(h : ∀ i, AlgebraicIndependent R ((↑) : s i → A)) : AlgebraicIndependent R ((↑) : (⋃ i, s i) → A) :=
by
refine algebraicIndependent_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))
