delete_comm — Mathlib

English

Deleting D1 then D2 yields the same result as deleting D2 then D1: M \\ D1 \\ D2 = M \\ D2 \\ D1.

Русский

Удаление D1 затем D2 эквивалентно удалению D2 затем D1: M \\ D1 \\ D2 = M \\ D2 \\ D1.

LaTeX

$$$(M\\setminus D_1)\\setminus D_2 = (M\\setminus D_2)\\setminus D_1$$$

Lean4

theorem delete_comm (M : Matroid α) (D₁ D₂ : Set α) : M ＼ D₁ ＼ D₂ = M ＼ D₂ ＼ D₁ := by
  rw [delete_delete, union_comm, delete_delete]

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