English
If I and J are independent in M and encard(I) < encard(J), then there exists an element e in J \\ I such that I ∪ {e} is independent.
Русский
Если I и J независимы в M и encard(I) < encard(J), то существует элемент e ∈ J \\ I такой, что I ∪ {e} независимо в M.
LaTeX
$$$\\exists e \\in J \\setminus I,\\ M.Indep(I \\cup \\{e\\})$$$
Lean4
/-- Any independent set can be extended into a larger independent set. -/
theorem augment (hI : M.Indep I) (hJ : M.Indep J) (hIJ : I.encard < J.encard) : ∃ e ∈ J \ I, M.Indep (insert e I) :=
by
by_contra! he
have hb : M.IsBasis I (I ∪ J) :=
by
simp_rw [hI.isBasis_iff_forall_insert_dep subset_union_left, union_diff_left, mem_diff, and_imp, dep_iff,
insert_subset_iff, and_iff_left hI.subset_ground]
exact fun e heJ heI ↦ ⟨he e ⟨heJ, heI⟩, hJ.subset_ground heJ⟩
obtain ⟨J', hJ', hJJ'⟩ := hJ.subset_isBasis_of_subset I.subset_union_right
rw [← hJ'.encard_eq_encard hb] at hIJ
exact hIJ.not_ge (encard_mono hJJ')
