Theorems · Theorem · combinatorics

Matroid.ext_indep_disjoint_loops_coloops

∀ {α : Type u_1} {M₁ M₂ : Matroid α},
  M₁.E = M₂.E →
    M₁.loops = M₂.loops →
      M₁.coloops = M₂.coloops → (∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)) → M₁ = M₂

If two matroids agree on loops and coloops, and have the same independent sets after loops/coloops are removed, they are equal.

Defined in

Mathlib.Combinatorics.Matroid.Loop

Cited by

0 results in Mathlib

Foundations

Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound