isRestriction_iff_exists_eq_delete

English

For matroids M and N, N ≤_r M if and only if there exists D ⊆ E(M) with N = M \\ D.

Русский

Для матроидов M и N выполняется: N ≤_r M тогда и только тогда, когда существует D ⊆ E(M) такое, что N = M \\ D.

LaTeX

$$$N\\le_r M \\iff \\exists D\\subseteq M.E,\\ N = M\\setminus D$$$

Lean4

theorem isRestriction_iff_exists_eq_delete : N ≤r M ↔ ∃ D ⊆ M.E, N = M ＼ D :=
  ⟨IsRestriction.exists_eq_delete, by rintro ⟨D, -, rfl⟩; apply delete_isRestriction⟩

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