English
Let M be a matroid on a set α and assume I is a basis of X in M (I is a basis for X inside M). Then for any sets J and X, the subset J \\ X is independent in the contracted matroid M / X if and only if the union (J \\ X) ∪ I is independent in M.
Русский
Пусть M — матроид на множествах α, и пусть I является базисом X в M. Тогда для любых множеств J и X подмножество J \ X независимо в сокращенном матроиде M / X тогда и только тогда, когда объединение (J \ X) ∪ I независимо в M.
LaTeX
$$$(M / X).Indep(J \\ X) \\iff M.Indep((J \\ X) \\cup I)$$$
Lean4
theorem contract_indep_diff_iff (hI : M.IsBasis' I X) : (M / X).Indep (J \ X) ↔ M.Indep ((J \ X) ∪ I) := by
rw [hI.contract_indep_iff, and_iff_left disjoint_sdiff_right]