delete_contract_delete' — Mathlib

English

Another variant expressing the action of deleting and contracting without disjointness assumptions.

Русский

Еще один вариант выражения действий удаления и сжатия без предположений непересечения.

LaTeX

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

Lean4

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

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