Theorems · Theorem · combinatorics

Matroid.IsCircuit.elimination

∀ {α : Type u_1} {M : Matroid α} {C₁ C₂ : Set α},
  M.IsCircuit C₁ → M.IsCircuit C₂ → C₁ ≠ C₂ → ∀ (e : α), ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C

The circuit elimination axiom : for any pair of distinct circuits C₁, C₂ and any e, some circuit is contained in (C₁ ∪ C₂) \ {e}. This is one of the axioms when defining a finitary matroid via circuits; as an axiom, it is usually stated with the extra assumption that e ∈ C₁ ∩ C₂.

Defined in

Mathlib.Combinatorics.Matroid.Circuit

Cited by

0 results in Mathlib

Foundations

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