English
Contracting by the closure of C is the same as contracting by C and then deleting elements in closure(C) \\ C.
Русский
Сокращение по замыканию C эквивалентно сокращению по C и последующему удалению элементов closure(C) \\ C.
LaTeX
$$M ／ M.closure C = (M ／ C).delete (M.closure C \\ C)$$
Lean4
/-- Contracting the closure of a set is the same as contracting the set,
and then deleting the rest of its elements. -/
theorem contract_closure_eq_contract_delete (M : Matroid α) (C : Set α) : M ／ M.closure C = M ／ C ＼ (M.closure C \ C) :=
by
wlog hCE : C ⊆ M.E with aux
·
rw [← M.contract_inter_ground_eq C, ← closure_inter_ground, aux _ _ inter_subset_right, diff_inter,
diff_eq_empty.2 (M.closure_subset_ground _), union_empty]
obtain ⟨I, hI⟩ := M.exists_isBasis C
rw [hI.isBasis_closure_right.contract_eq_contract_delete, hI.contract_eq_contract_delete, delete_delete, union_comm,
diff_union_diff_cancel (M.subset_closure C) hI.subset]
