contract_delete_comm — Mathlib

English

If C ⊆ R, then (M | R) contract C = (M contract C) | (R \ C).

Русский

Если C ⊆ R, то (M ограничено R) сжатие C равно (M сжатие C) ограничено R \ C.

LaTeX

$$(M | R).contract C = (M.contract C) | (R \ C)$$

Lean4

/-- Contraction and deletion commute for disjoint sets. -/
theorem contract_delete_comm (M : Matroid α) (hCD : Disjoint C D) : M ／ C ＼ D = M ＼ D ／ C :=
  by
  wlog hCE : C ⊆ M.E generalizing C with aux
  ·
    rw [← contract_inter_ground_eq, aux (hCD.mono_left inter_subset_left) inter_subset_right, contract_eq_contract_iff,
      inter_assoc, delete_ground, inter_eq_self_of_subset_right diff_subset]
  rw [delete_eq_restrict, delete_eq_restrict, contract_ground, diff_diff_comm,
    restrict_contract_eq_contract_restrict _ (by simpa [hCE, subset_diff])]

Похожие утверждения