English
Let I be independent in M, and let {X_i}_{i∈ι} be a family of subsets indexed by a nonempty ι. If for every i, X_i ∩ I is a basis of X_i, then (⋂_i X_i) ∩ I is a basis of ⋂_i X_i.
Русский
Пусть I независимо в M, а {X_i}_{i∈ι} — семейство подмножеств, индексируемое не пустым ι. Если для каждого i множество X_i ∩ I является базисом X_i, то (⋂_i X_i) ∩ I является базисом ⋂_i X_i.
LaTeX
$$$\text{Assume } ι \text{ nonempty. If } hI:\ M.Indep I \text{ and } h:\ \forall i,\ M.IsBasis((X_i\\cap I),X_i),\\\text{ then } M.IsBasis\\Big((\\bigcap_i X_i)\\cap I\\Big)\\Big(\\bigcap_i X_i\\Big).$$$
Lean4
theorem inter_isBasis_iInter [Nonempty ι] {X : ι → Set α} (hI : M.Indep I) (h : ∀ i, M.IsBasis ((X i) ∩ I) (X i)) :
M.IsBasis ((⋂ i, X i) ∩ I) (⋂ i, X i) := by
convert
hI.inter_isBasis_biInter (ι := PLift ι) univ_nonempty (X := fun i ↦ X i.down)
(by simpa using fun (i : PLift ι) ↦ h i.down) <;>
· simp only [mem_univ, iInter_true]
exact (iInter_plift_down X).symm
