Theorems · Theorem · combinatorics

Matroid.IsBase.mem_fundCocircuit_iff_mem_fundCircuit

∀ {α : Type u_1} {M : Matroid α} {B : Set α} {e f : α}, M.IsBase B → (e ∈ M.fundCocircuit f B ↔ f ∈ M.fundCircuit e B)

Fundamental circuits and cocircuits of a base B play dual roles; e belongs to the fundamental cocircuit for B and f if and only if f belongs to the fundamental circuit for e and B. This statement isn't so reasonable unless f ∈ B and e ∉ B, but holds due to junk values even without these assumptions.

Defined in

Mathlib.Combinatorics.Matroid.Circuit

Cited by

0 results in Mathlib

Foundations

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