dual_delete — Mathlib

English

The dual of the matroid obtained by deleting X equals the contraction of X in the dual: (M \\ X)^* = M^* / X.

Русский

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

LaTeX

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

Lean4

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

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