English
If I is independent and not maximal, and B is maximal independent, then there exists x ∈ B \\ I such that I ∪ {x} is independent.
Русский
Если I независимо и не максимально, и B максимально независимо, тогда существует x ∈ B \\ I такое, что I ∪ {x} независимо.
LaTeX
$$M.Indep(I) \\land ¬Maximal M.Indep(I) \\land Maximal M.Indep(B) \\Rightarrow ∃ x ∈ B \\setminus I, M.Indep(I \\cup \\{x\\})$$
Lean4
/-- This is the same as `Indep.exists_insert_of_not_isBase`, but phrased so that
it is defeq to the augmentation axiom for independent sets. -/
theorem exists_insert_of_not_maximal (M : Matroid α) ⦃I B : Set α⦄ (hI : M.Indep I) (hInotmax : ¬Maximal M.Indep I)
(hB : Maximal M.Indep B) : ∃ x ∈ B \ I, M.Indep (insert x I) :=
by
simp only [maximal_subset_iff, hI, not_and, not_forall, exists_prop, true_imp_iff] at hB hInotmax
refine hI.exists_insert_of_not_isBase (fun hIb ↦ ?_) ?_
· obtain ⟨I', hII', hI', hne⟩ := hInotmax
exact hne <| hIb.eq_of_subset_indep hII' hI'
exact hB.1.isBase_of_maximal fun J hJ hBJ ↦ hB.2 hJ hBJ
