English
If I is independent, not a base, and B is a base, then there exists an element e in B \\ I such that I ∪ {e} is independent.
Русский
Если I независимо и не является базой, и B является базой, существует элемент e ∈ B \\ I такой, что I ∪ {e} независимо.
LaTeX
$$M.Indep(I) \\land ¬M.IsBase(I) \\land M.IsBase(B) \\Rightarrow ∃ e ∈ B \\setminus I, M.Indep(I \\cup \\{e\\})$$
Lean4
theorem exists_insert_of_not_isBase (hI : M.Indep I) (hI' : ¬M.IsBase I) (hB : M.IsBase B) :
∃ e ∈ B \ I, M.Indep (insert e I) :=
by
obtain ⟨B', hB', hIB'⟩ := hI.exists_isBase_superset
obtain ⟨x, hxB', hx⟩ := exists_of_ssubset (hIB'.ssubset_of_ne (by (rintro rfl; exact hI' hB')))
by_cases hxB : x ∈ B
· exact ⟨x, ⟨hxB, hx⟩, hB'.indep.subset (insert_subset hxB' hIB')⟩
obtain ⟨e, he, hBase⟩ := hB'.exchange hB ⟨hxB', hxB⟩
exact
⟨e, ⟨he.1, notMem_subset hIB' he.2⟩, indep_iff.2 ⟨_, hBase, insert_subset_insert (subset_diff_singleton hIB' hx)⟩⟩
