Theorems · Theorem · combinatorics

Matroid.IsCircuit.strong_multi_elimination_insert

∀ {α : Type u_1} {M : Matroid α} {ι : Type u_2} {J : Set α} (x : ι → α) (I : ι → Set α) (z : α),
  (∀ (i : ι), x i ∉ I i) →
    (∀ (i : ι), M.IsCircuit (insert (x i) (I i))) →
      M.IsCircuit (J ∪ Set.range x) → z ∈ J → (∀ (i : ι), z ∉ I i) → ∃ C' ⊆ J ∪ ⋃ i, I i, M.IsCircuit C' ∧ z ∈ C'

A version of Matroid.IsCircuit.strong_multi_elimination that is phrased using insertion.

Defined in

Mathlib.Combinatorics.Matroid.Circuit

Cited by

1 results in Mathlib

Foundations

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