delete_isColoop_iff — Mathlib

English

(M \ D).IsColoop e iff e lies in E(M) and e ∉ D and e is not forced by closure condition.

Русский

Петля после удаления D эквивалентна условию с e: e ∈ E(M), e ∉ D, и не нарушено замыканием.

LaTeX

$$$ (M \setminus D).IsColoop(e) \iff e \notin M.closure((M.E \ D) \ {e}) \land e \in M.E \land e \notin D $$$

Lean4

theorem delete_isColoop_iff (M : Matroid α) (D : Set α) :
    (M ＼ D).IsColoop e ↔ e ∉ M.closure ((M.E \ D) \ { e }) ∧ e ∈ M.E ∧ e ∉ D :=
  by
  rw [delete_eq_restrict, restrict_isColoop_iff diff_subset, mem_diff, and_congr_left_iff, and_imp]
  simp

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