English
If for every i, I_i is a basis of X_i, and the union of all I_i is independent, then the union of all I_i is a basis of the union of all X_i.
Русский
Если для каждого i множество I_i является базисом X_i, и объединение всех I_i независимо, тогда объединение всех I_i является базисом объединения всех X_i.
LaTeX
$$$ \\left( \\forall i, M.IsBasis(I_i, X_i) \\right) \\land M.Indep\\left( \\bigcup_i I_i \\right) \\Rightarrow M.IsBasis\\left( \\bigcup_i I_i, \\bigcup_i X_i \\right) $$$
Lean4
theorem iUnion_isBasis_iUnion {ι : Type _} (X I : ι → Set α) (hI : ∀ i, M.IsBasis (I i) (X i))
(h_ind : M.Indep (⋃ i, I i)) : M.IsBasis (⋃ i, I i) (⋃ i, X i) :=
by
refine h_ind.isBasis_of_forall_insert (iUnion_subset (fun i ↦ (hI i).subset.trans (subset_iUnion _ _))) ?_
rintro e ⟨⟨_, ⟨⟨i, hi, rfl⟩, (hes : e ∈ X i)⟩⟩, he'⟩
rw [mem_iUnion, not_exists] at he'
refine ((hI i).insert_dep ⟨hes, he' _⟩).superset (insert_subset_insert (subset_iUnion _ _)) ?_
rw [insert_subset_iff, iUnion_subset_iff, and_iff_left (fun i ↦ (hI i).indep.subset_ground)]
exact (hI i).subset_ground hes
