contract_delete_contract_delete' — Mathlib

English

A variant showing how nested contractions and deletions can be rearranged with unions and multiset operations.

Русский

Вариант, демонстрирующий перестановку вложенных сжатий и удалений с объединениями.

LaTeX

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

Lean4

/-- A version of `contract_delete_contract_delete` without the disjointness hypothesis,
and hence a less simple RHS. -/
theorem contract_delete_contract_delete' (M : Matroid α) (C D C' D' : Set α) :
    M ／ C ＼ D ／ C' ＼ D' = M ／ (C ∪ C' \ D) ＼ (D ∪ D') := by rw [contract_delete_contract', delete_delete]

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