English
Let I be an independent set in M. For a nonempty index set A and a family of subsets {X_i} (i in A), if for every i in A the set X_i ∩ I is a basis of X_i, then (⋂_{i∈A} X_i) ∩ I is a basis for ⋂_{i∈A} X_i.
Русский
Пусть I — независимое множество в M. Пусть A — ненуловой индексный множество и есть семейство множеств {X_i} (i ∈ A). Если для каждого i ∈ A множество X_i ∩ I является базисом X_i, то ⋂_{i∈A} X_i, пересечение с I, является базисом ⋂_{i∈A} X_i.
LaTeX
$$$\text{If } hI:\ M \\text{Indep } I,\ hA:\ A\\neq \\varnothing,\ h:\ \\forall i\\in A,\\ M.IsBasis\\Big((X_i\\cap I),\\ X_i\\Big)\\text{, then } M.IsBasis\\Big(\\bigl(\\bigcap_{i\\in A} X_i\\bigr)\\cap I\\,,\\ \\bigcap_{i\\in A} X_i\\Big).$$$
Lean4
theorem inter_isBasis_biInter {ι : Type*} (hI : M.Indep I) {X : ι → Set α} {A : Set ι} (hA : A.Nonempty)
(h : ∀ i ∈ A, M.IsBasis ((X i) ∩ I) (X i)) : M.IsBasis ((⋂ i ∈ A, X i) ∩ I) (⋂ i ∈ A, X i) :=
by
refine (hI.inter_left _).isBasis_of_subset_of_subset_closure inter_subset_left ?_
simp_rw [← biInter_inter hA,
closure_biInter_eq_biInter_closure_of_biUnion_indep hA (I := fun i ↦ (X i) ∩ I) (hI.subset (by simp)),
subset_iInter_iff]
exact fun i hiA ↦ (biInter_subset_of_mem hiA).trans (h i hiA).subset_closure
