dual_delete_contract — Mathlib

English

Deleting X and then contracting Y, when dualized, corresponds to deleting Y and contracting X in the dual: (M \\ X) / Y dual equals M^* \\ X / Y.

Русский

Удаление X затем сокращение Y, после двойственности, соответствует удалению Y и сокращению X в двойственном: (M \\ X) / Y^{*} = M^{*} \\ X / Y.

LaTeX

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

Lean4

theorem dual_delete_contract (M : Matroid α) (X Y : Set α) : (M ＼ X ／ Y)✶ = M✶ ／ X ＼ Y := by simp

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