English
If I is independent, closure of an sInter equals the biInter of closures over a family of subsets.
Русский
Если I независим, то cl(⋂ Js) = ⋂ cl(Js) над семейством Js ⊆ I.
LaTeX
$$$\operatorname{Indep}(I) \rightarrow \operatorname{cl}\left(\bigcap_{J \in \mathcal{J}} J\right) = \bigcap_{J \in \mathcal{J}} \operatorname{cl}(J)$$$
Lean4
/-- For a nonempty collection of subsets of a given independent set,
the closure of the intersection is the intersection of the closure. -/
theorem closure_sInter_eq_biInter_closure_of_forall_subset {Js : Set (Set α)} (hI : M.Indep I) (hne : Js.Nonempty)
(hIs : ∀ J ∈ Js, J ⊆ I) : M.closure (⋂₀ Js) = (⋂ J ∈ Js, M.closure J) :=
by
rw [subset_antisymm_iff, subset_iInter₂_iff]
have hiX : ⋂₀ Js ⊆ I := (sInter_subset_of_mem hne.some_mem).trans (hIs _ hne.some_mem)
have hiI := hI.subset hiX
refine ⟨fun X hX ↦ M.closure_subset_closure (sInter_subset_of_mem hX), fun e he ↦ by_contra fun he' ↦ ?_⟩
rw [mem_iInter₂] at he
have heEI : e ∈ M.E \ I :=
by
refine ⟨M.closure_subset_ground _ (he _ hne.some_mem), fun heI ↦ he' ?_⟩
refine mem_closure_of_mem _ (fun X hX' ↦ ?_) hiI.subset_ground
rw [← hI.closure_inter_eq_self_of_subset (hIs X hX')]
exact ⟨he X hX', heI⟩
rw [hiI.notMem_closure_iff_of_notMem (notMem_subset hiX heEI.2)] at he'
obtain ⟨J, hJI, heJ⟩ :=
he'.subset_isBasis_of_subset (insert_subset_insert hiX) (insert_subset heEI.1 hI.subset_ground)
have hIb : M.IsBasis I (insert e I) := by
rw [hI.insert_isBasis_iff_mem_closure]
exact (M.closure_subset_closure (hIs _ hne.some_mem)) (he _ hne.some_mem)
obtain ⟨f, hfIJ, hfb⟩ := hJI.exchange hIb ⟨heJ (mem_insert e _), heEI.2⟩
obtain rfl :=
hI.eq_of_isBasis
(hfb.isBasis_subset (insert_subset hfIJ.1 (by (rw [diff_subset_iff, singleton_union]; exact hJI.subset)))
(subset_insert _ _))
refine hfIJ.2 (heJ (mem_insert_of_mem _ fun X hX' ↦ by_contra fun hfX ↦ ?_))
obtain (hd | heX) := ((hI.subset (hIs X hX')).mem_closure_iff).mp (he _ hX')
· refine (hJI.indep.subset (insert_subset (heJ (mem_insert _ _)) ?_)).not_dep hd
specialize hIs _ hX'
rw [← singleton_union, ← diff_subset_iff, diff_singleton_eq_self hfX] at hIs
exact hIs.trans diff_subset
exact heEI.2 (hIs _ hX' heX)
