English
If B is a base, f ∉ B, and I is independent with insert f (B \ { e }), then the new set is a base.
Русский
Если B — база, f ∉ B, и I независимо (insert f (B \ { e })), тогда новая система является базой.
LaTeX
$$$ M.IsBase B \rightarrow (f \notin B) \rightarrow M.Indep (\text{insert } f (B \ { e })) \rightarrow M.IsBase (\text{insert } f (B \ { e }))$$$
Lean4
/-- If the difference of two IsBases is a singleton, then they differ by an insertion/removal -/
theorem eq_exchange_of_diff_eq_singleton (hB : M.IsBase B) (hB' : M.IsBase B') (h : B \ B' = { e }) :
∃ f ∈ B' \ B, B' = (insert f B) \ { e } :=
by
obtain ⟨f, hf, hb⟩ := hB.exchange hB' (h.symm.subset (mem_singleton e))
have hne : f ≠ e := by rintro rfl; exact hf.2 (h.symm.subset (mem_singleton f)).1
rw [insert_diff_singleton_comm hne] at hb
refine ⟨f, hf, (hb.eq_of_subset_isBase hB' ?_).symm⟩
rw [diff_subset_iff, insert_subset_iff, union_comm, ← diff_subset_iff, h, and_iff_left rfl.subset]
exact Or.inl hf.1
