English
If two bases B and B' differ by a singleton, then there exists an element f in B'\B such that B' equals (insert f B) \ { e }.
Русский
Если две базы B и B' различаются на единичное множество, существует элемент f ∈ B'\B такой, что B' = (insert f B) \ { e }.
LaTeX
$$$ M.IsBase B \rightarrow M.IsBase B' \rightarrow (B \setminus B') = \{ e \} \Rightarrow \exists f \in B' \setminus B, B' = (\operatorname{insert} f B) \setminus \{ e \}$$$
Lean4
theorem exchange_isBase_of_indep (hB : M.IsBase B) (hf : f ∉ B) (hI : M.Indep (insert f (B \ { e }))) :
M.IsBase (insert f (B \ { e })) :=
by
obtain ⟨B', hB', hIB'⟩ := hI.exists_isBase_superset
have hcard := hB'.encard_diff_comm hB
rw [insert_subset_iff, ← diff_eq_empty, diff_diff_comm, diff_eq_empty, subset_singleton_iff_eq] at hIB'
obtain ⟨hfB, (h | h)⟩ := hIB'
· rw [h, encard_empty, encard_eq_zero, eq_empty_iff_forall_notMem] at hcard
exact (hcard f ⟨hfB, hf⟩).elim
rw [h, encard_singleton, encard_eq_one] at hcard
obtain ⟨x, hx⟩ := hcard
obtain (rfl : f = x) := hx.subset ⟨hfB, hf⟩
simp_rw [← h, ← singleton_union, ← hx, sdiff_sdiff_right_self, inf_eq_inter, inter_comm B, diff_union_inter]
exact hB'
