contract_delete_contract' — Mathlib

English

A generalized form: contract followed by delete and then contract again equals a single contract with unions and sdiffs of the sets.

Русский

Обобщенная форма: сжатие, затем удаление и снова сжатие равны одному сжатию с объединениями и разностями множеств.

LaTeX

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

Lean4

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

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