English
The closure after contraction satisfies (M ／ C).closure X = M.closure (X ∪ C) \\ C.
Русский
Замыкание после сокращения удовлетворяет $(M ／ C).closure X = M.closure (X ∪ C) \\ C$.
LaTeX
$$$(M ／ C).closure X = M.closure (X \\cup C) \\ C$$
Lean4
@[simp]
theorem contract_closure_eq (M : Matroid α) (C X : Set α) : (M ／ C).closure X = M.closure (X ∪ C) \ C :=
by
rw [← diff_union_inter (M.closure (X ∪ C) \ C) X, diff_diff, union_comm C, ← contract_loops_eq, union_comm X, ←
contract_contract, contract_loops_eq, subset_antisymm_iff, union_subset_iff, and_iff_right diff_subset, ←
diff_subset_iff]
simp only [sdiff_sdiff_right_self, inf_eq_inter, subset_inter_iff, inter_subset_right, and_true]
refine
⟨fun e ⟨he, he'⟩ ↦
⟨mem_closure_of_mem' _ (.inr he') (mem_ground_of_mem_closure he).1, (closure_subset_ground _ _ he).2⟩,
fun e ⟨⟨he, heC⟩, he'⟩ ↦ mem_closure_of_mem' _ he' ⟨M.closure_subset_ground _ he, heC⟩⟩
