contract_eq_delete_of_subset_coloops

English

If X is a subset of the coloops of M, contracting by X is the same as deleting X.

Русский

Если X ⊆ колопы матроида M, сокращение по X эквивалентно удалению X.

LaTeX

$$$X \\subseteq M.coloops \\Rightarrow M / X = M \\setminus X$$$

Lean4

theorem contract_eq_delete_of_subset_coloops (hX : X ⊆ M.coloops) : M ／ X = M ＼ X := by
  rw [← dual_inj, dual_delete, contract_eq_delete_of_subset_loops hX, dual_contract]

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