English
Let M be a matroid on α and I ⊆ X. Then I is a basis of X if and only if every element e in X \\ I makes I ∪ {e} dependent.
Русский
Пусть M — матроид на α и I ⊆ X. Тогда I является базисом X тогда и только тогда, когда для каждого элемента e ∈ X \ I множество I ∪ {e} зависимо в M.
LaTeX
$$$ M.IsBasis I X \\iff \\forall e \\in X \\setminus I,\\ M.Dep(I \\cup \\{e\\}) $$$
Lean4
theorem isBasis_iff_forall_insert_dep (hI : M.Indep I) (hIX : I ⊆ X) :
M.IsBasis I X ↔ ∀ e ∈ X \ I, M.Dep (insert e I) :=
by
rw [IsBasis, maximal_iff_forall_insert (fun I J hI hIJ ↦ ⟨hI.1.subset hIJ, hIJ.trans hI.2⟩)]
simp only [hI, hIX, and_self, insert_subset_iff, and_true, not_and, true_and, mem_diff, and_imp, Dep,
hI.subset_ground]
exact
⟨fun h e heX heI ↦ ⟨fun hi ↦ h.1 e heI hi heX, h.2 heX⟩, fun h ↦
⟨fun e heI hi heX ↦ (h e heX heI).1 hi, fun e heX ↦
(em (e ∈ I)).elim (fun h ↦ hI.subset_ground h) fun heI ↦ (h _ heX heI).2⟩⟩
