delete_delete_eq_delete_diff — Mathlib

English

Deleting D1 then D2 equals deleting D1 while removing D2 \ D1: M \\ D1 \\ D2 = M \\ D1 \\ (D2 \\ D1).

Русский

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

LaTeX

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

Lean4

theorem delete_delete_eq_delete_diff (M : Matroid α) (D₁ D₂ : Set α) : M ＼ D₁ ＼ D₂ = M ＼ D₁ ＼ (D₂ \ D₁) := by simp

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