Theorems · Theorem · combinatorics

Matroid.IsCircuit.strong_multi_elimination

∀ {α : Type u_1} {M : Matroid α} {ι : Type u_2} {C₀ : Set α},
  M.IsCircuit C₀ →
    ∀ (x : ι → α) (C : ι → Set α) (z : α),
      (∀ (i : ι), M.IsCircuit (C i)) →
        (∀ (i : ι), x i ∈ C₀) →
          (∀ (i : ι), x i ∈ C i) →
            (∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i') →
              z ∈ C₀ → (∀ (i : ι), z ∉ C i) → ∃ C' ⊆ (C₀ ∪ ⋃ i, C i) \ Set.range x, M.IsCircuit C' ∧ z ∈ C'

A generalization of the strong circuit elimination axiom Matroid.IsCircuit.strong_elimination to an infinite collection of circuits. It states that, given a circuit C₀, an arbitrary collection C : ι → Set α of circuits, an element x i of C₀ ∩ C i for each i, and an element z ∈ C₀ outside all the C i, the union of C₀ and the C i contains a circuit containing z but none of the x i. This is one of the axioms when defining infinite matroids via circuits. TODO : A similar statement will hold even when all mentions of z are removed.

Defined in

Mathlib.Combinatorics.Matroid.Circuit

Cited by

2 results in Mathlib

Foundations

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