contract_delete_contract — Mathlib

English

For disjoint C and K, contraction by C then deletion by K equals deletion then contraction with adjusted sets.

Русский

При непересечении C и K сжатие по C затем удаление по K равно удалению сначала и сжатию по корректированному набору.

LaTeX

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

Lean4

theorem contract_delete_contract (M : Matroid α) (C D C' : Set α) (h : Disjoint C' D) :
    M ／ C ＼ D ／ C' = M ／ (C ∪ C') ＼ D := by rw [contract_delete_contract', sdiff_eq_left.mpr h]

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