English
In a finitary matroid, if X is finite and X ⊆ closure(Y), then there exists I ⊆ Y with I finite, I independent, and X ⊆ closure(I).
Русский
В финитарном матроидe, если X конечно и X ⊆ замыкание(Y), то существует I ⊆ Y такое, что I конечное, I независимое и X ⊆ замыкание(I).
LaTeX
$$$X \text{ finite} \land X \subseteq \mathrm{cl}_M(Y) \Rightarrow \exists I \subseteq Y,\ I \text{ finite} \land \mathrm{Indep}_M(I) \land X \subseteq \mathrm{cl}_M(I)$$$
Lean4
/-- In a finitary matroid, each finite set `X` spanned by a set `Y` is in fact
spanned by a finite independent subset of `Y`. -/
theorem exists_subset_finite_closure_of_subset_closure [M.Finitary] (hX : X.Finite) (hXY : X ⊆ M.closure Y) :
∃ I ⊆ Y, I.Finite ∧ M.Indep I ∧ X ⊆ M.closure I :=
by
suffices aux : ∃ T ⊆ Y, T.Finite ∧ X ⊆ M.closure T
by
obtain ⟨T, hT, hTfin, hXT⟩ := aux
obtain ⟨I, hI⟩ := M.exists_isBasis' T
exact ⟨_, hI.subset.trans hT, hTfin.subset hI.subset, hI.indep, by rwa [hI.closure_eq_closure]⟩
refine Finite.induction_on_subset X hX ⟨∅, by simp⟩ (fun {e Z} heX _ heZ ⟨T, hTY, hTfin, hT⟩ ↦ ?_)
obtain ⟨S, hSY, hSfin, -, heS⟩ := exists_mem_finite_closure_of_mem_closure (hXY heX)
exact
⟨S ∪ T, union_subset hSY hTY, hSfin.union hTfin,
insert_subset (M.closure_mono subset_union_left heS) (hT.trans (M.closure_mono subset_union_right))⟩
