delete_eq_delete_iff — Mathlib

English

Two deletions M \\ D1 and M \\ D2 are equal if and only if D1 ∩ E(M) = D2 ∩ E(M).

Русский

Удаление M \\ D1 совпадает с удалением M \\ D2 тогда, когда D1 ∩ E(M) = D2 ∩ E(M).

LaTeX

$$$M\\setminus D_1 = M\\setminus D_2 \\iff D_1\\cap M.E = D_2\\cap M.E$$$

Lean4

theorem delete_eq_delete_iff {D₁ D₂ : Set α} : M ＼ D₁ = M ＼ D₂ ↔ D₁ ∩ M.E = D₂ ∩ M.E :=
  by
  rw [← delete_inter_ground_eq, ← M.delete_inter_ground_eq D₂]
  refine ⟨fun h ↦ ?_, fun h ↦ by rw [h]⟩
  apply_fun (M.E \ Matroid.E ·) at h
  simp_rw [delete_ground, diff_diff_cancel_left inter_subset_right] at h
  assumption

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