dual_delete_dual — Mathlib

English

The dual of the matroid obtained by deleting X is equal to the matroid obtained by contracting X in the dual: (M^* \\ X)^* = M / X.

Русский

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

LaTeX

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

Lean4

theorem dual_delete_dual (M : Matroid α) (X : Set α) : (M✶ ＼ X)✶ = M ／ X :=
  rfl

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