restrict_contract_eq_contract_restrict

English

Restriction and contraction commute under disjointness: (M ⟂ R) contract C equals (M contract C) restricted to R \ C.

Русский

Ограничение и сжатие взаимно приводят к эквивалентности: (M ⟂ R).contract C = (M.contract C).restrict(R \ C).

LaTeX

$$(M ⟂ R).contract C = (M.contract C).restrict(R \ C)$$

Lean4

theorem restrict_contract_eq_contract_restrict (M : Matroid α) (hCR : C ⊆ R) : (M ↾ R) ／ C = (M ／ C) ↾ (R \ C) :=
  by
  rw [contract_restrict_eq_restrict_contract _ disjoint_sdiff_right]
  simp [union_eq_self_of_subset_right hCR]

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