dual_contract — Mathlib

English

The dual of the contracted matroid M / X equals the dual of M with a deletion of X: (M / X)^* = M^* \\ X.

Русский

Двойственный сокращенного матроида M / X равен двойственному матроиду M без элемента X: (M / X)^* = M^* \\ X.

LaTeX

$$$ (M / X)^{*} = M^{*} \\ X $$$

Lean4

@[simp]
theorem dual_contract (M : Matroid α) (X : Set α) : (M ／ X)✶ = M✶ ＼ X := by rw [← dual_delete_dual, dual_dual]

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