Theorems · Theorem · combinatorics

Matroid.isColoop_tfae

∀ {α : Type u_1} (M : Matroid α) (e : α),
  [M.IsColoop e, e ∈ M.coloops, M.IsCocircuit {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B,
      (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E, ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X,
      ¬M.Spanning (M.E \ {e})].TFAE

Defined in

Mathlib.Combinatorics.Matroid.Loop

Cited by

4 results in Mathlib

Foundations

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