delete_contract_comm' — Mathlib

English

Variant without the disjointness assumption: (M.delete D).contract C = M.contract (C \ D) .delete D.

Русский

Вариант без предположения о непересечении: (M.delete D).contract C = M.contract (C \ D) .delete D.

LaTeX

$$(M.delete D).contract C = M.contract (C \ D) .delete D$$

Lean4

/-- A version of `delete_contract_comm'` without the disjointness hypothesis,
and hence a less simple RHS. -/
theorem delete_contract_comm' (M : Matroid α) (D C : Set α) : M ＼ D ／ C = M ／ (C \ D) ＼ D := by
  rw [delete_contract_eq_diff, ← contract_delete_comm _ disjoint_sdiff_left]

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