English
In a finitary matroid M, if e lies in the closure of a set X, then e lies in the closure of some finite independent subset of X.
Русский
В финитарном матроиде M, если e принадлежит замыканию множества X, то существует конечное независимое подмножество I ⊆ X такое, что e ∈ замыкание I.
LaTeX
$$$e \in \mathrm{cl}_M(X) \Rightarrow \exists I \subseteq X,\ I \text{ finite} \land \mathrm{Indep}_M(I) \land e \in \mathrm{cl}_M(I)$$$
Lean4
/-- In a finitary matroid, every element spanned by a set `X` is in fact
spanned by a finite independent subset of `X`. -/
theorem exists_mem_finite_closure_of_mem_closure [M.Finitary] (he : e ∈ M.closure X) :
∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I :=
by
by_cases heY : e ∈ X
· obtain ⟨J, hJ⟩ := M.exists_isBasis { e }
exact
⟨J, hJ.subset.trans (by simpa), (finite_singleton e).subset hJ.subset, hJ.indep, by simpa using hJ.subset_closure⟩
obtain ⟨C, hCs, hC, heC⟩ := exists_isCircuit_of_mem_closure he heY
exact ⟨C \ { e }, by simpa, hC.finite.diff, hC.diff_singleton_indep heC, hC.mem_closure_diff_singleton_of_mem heC⟩
