contract_delete_comm' — Mathlib

English

A variant without the disjointness hypothesis: M ／ C ＼ D = M ／ (D \ C) ／ C.

Русский

Вариант без предположения о непересечении: M ／ C ＼ D = M ／ (D \ C) ／ C.

LaTeX

$$M / C \\ D = M / (D \ C) \\ C$$

Lean4

/-- A version of `contract_delete_comm` without the disjointness hypothesis,
and hence a less simple RHS. -/
theorem contract_delete_comm' (M : Matroid α) (C D : Set α) : M ／ C ＼ D = M ＼ (D \ C) ／ C := by
  rw [contract_delete_diff, contract_delete_comm _ disjoint_sdiff_right]

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