Theorems · Theorem · combinatorics

Matroid.IsCircuit.strong_multi_elimination_set

∀ {α : Type u_1} {M : Matroid α} {C₀ : Set α},
  M.IsCircuit C₀ →
    ∀ (X : Set α) (S : Set (Set α)) (z : α),
      (∀ C ∈ S, M.IsCircuit C) →
        X ⊆ C₀ →
          (∀ x ∈ X, ∃ C ∈ S, C ∩ X = {x}) → z ∈ C₀ → (∀ C ∈ S, z ∉ C) → ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.IsCircuit C' ∧ z ∈ C'

A version of Circuit.strong_multi_elimination where the collection of circuits is a Set (Set α) and the distinguished elements are a Set α, rather than both being indexed.

Defined in

Mathlib.Combinatorics.Matroid.Circuit

Cited by

0 results in Mathlib

Foundations

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