English
If I \ {e} is independent and e ∈ I, then Indep((I \ {e}) ∪ {f} \ {e}) is equivalent to f ∈ E \ cl(I \ {e}) or f ∈ I.
Русский
Если I \ {e} независим и e ∈ I, тогда Indep((I \ {e}) ∪ {f} \ {e}) эквивалентно f ∈ E \ cl(I \ {e}) или f ∈ I.
LaTeX
$$$\operatorname{Indep}\bigl((I \{e\}) \cup \{f\} \setminus \{e\}\bigr) \iff f \in E \setminus \operatorname{cl}(I \setminus \{e\}) \lor f \in I$$$
Lean4
/-- This can be used for rewriting if the LHS is inside a binder and it is unknown
whether `f = e`. -/
theorem insert_diff_indep_iff (hI : M.Indep (I \ { e })) (heI : e ∈ I) :
M.Indep (insert f I \ { e }) ↔ f ∈ M.E \ M.closure (I \ { e }) ∨ f ∈ I :=
by
obtain rfl | hne := eq_or_ne e f
· simp [hI, heI]
rw [← insert_diff_singleton_comm hne.symm, hI.insert_indep_iff, mem_diff_singleton, and_iff_left hne.symm]
