Matroid IsCircuits

A 'Circuit' of a matroid M is a minimal set C that is dependent in M. A matroid is determined by its set of circuits, and often the circuits offer a more compact description of a matroid than the collection of independent sets or bases. In matroids arising from graphs, circuits correspond to graphical cycles.

Main Declarations

• Matroid.IsCircuit M C means that C is minimally dependent in M.
• For an Independent set I whose closure contains an element e ∉ I, Matroid.fundCircuit M e I is the unique circuit contained in insert e I.
• Matroid.Indep.fundCircuit_isCircuit states that Matroid.fundCircuit M e I is indeed a circuit.
• Circuit.eq_fundCircuit_of_subset states that Matroid.fundCircuit M e I is the unique circuit contained in insert e I.
• Matroid.dep_iff_superset_isCircuit states that the dependent subsets of the ground set are precisely those that contain a circuit.
• Matroid.ext_isCircuit : a matroid is determined by its collection of circuits.
• Matroid.IsCircuit.strong_multi_elimination : the strong circuit elimination rule for an infinite collection of circuits.
• Matroid.IsCircuit.strong_elimination : the strong circuit elimination rule for two circuits.
• Matroid.finitary_iff_forall_isCircuit_finite : finitary matroids are precisely those whose circuits are all finite.
• Matroid.IsCocircuit M C means that C is minimally dependent in M✶, or equivalently that M.E \ C is a hyperplane of M.
• Matroid.fundCocircuit M B e is the unique cocircuit that intersects the base B precisely in the element e.
• Base.mem_fundCocircuit_iff_mem_fundCircuit : e is in the fundamental circuit for B and f iff f is in the fundamental cocircuit for B and e.

Implementation Details

Since Matroid.fundCircuit M e I is only sensible if I is independent and e ∈ M.closure I \ I, to avoid hypotheses being explicitly included in the definition, junk values need to be chosen if either hypothesis fails. The definition is chosen so that the junk values satisfy M.fundCircuit e I = {e} for e ∈ I or e ∉ M.E and M.fundCircuit e I = insert e I if e ∈ M.E \ M.closure I. These make the useful statement e ∈ M.fundCircuit e I ⊆ insert e I true unconditionally.

def Matroid.IsCircuit {α : Type u_1} (M : Matroid α) (x : Set α) : Prop

A Circuit of M is a minimal dependent set in M

Equations

• M.IsCircuit = Minimal M.Dep

@[deprecated Matroid.IsCircuit (since := "2025-02-14")]

def Matroid.Circuit {α : Type u_1} (M : Matroid α) (x : Set α) : Prop

Alias of Matroid.IsCircuit.

---

A Circuit of M is a minimal dependent set in M

Equations

• @Matroid.Circuit = @Matroid.IsCircuit

theorem Matroid.isCircuit_def {α : Type u_1} {M : Matroid α} {C : Set α} : M.IsCircuit C ↔ Minimal M.Dep C

theorem Matroid.IsCircuit.dep {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) : M.Dep C

theorem Matroid.IsCircuit.not_indep {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) : ¬M.Indep C

theorem Matroid.IsCircuit.minimal {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) : Minimal M.Dep C

theorem Matroid.IsCircuit.subset_ground {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) : C ⊆ M.E

theorem Matroid.IsCircuit.nonempty {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) : C.Nonempty

theorem Matroid.empty_not_isCircuit {α : Type u_1} (M : Matroid α) : ¬M.IsCircuit ∅

theorem Matroid.isCircuit_iff {α : Type u_1} {M : Matroid α} {C : Set α} : M.IsCircuit C ↔ M.Dep C ∧ ∀ ⦃D : Set α⦄, M.Dep D → D ⊆ C → D = C

theorem Matroid.IsCircuit.ssubset_indep {α : Type u_1} {M : Matroid α} {C X : Set α} (hC : M.IsCircuit C) (hXC : X ⊂ C) : M.Indep X

theorem Matroid.IsCircuit.minimal_not_indep {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) : Minimal (fun (x : Set α) => ¬M.Indep x) C

theorem Matroid.isCircuit_iff_minimal_not_indep {α : Type u_1} {M : Matroid α} {C : Set α} (hCE : C ⊆ M.E) : M.IsCircuit C ↔ Minimal (fun (x : Set α) => ¬M.Indep x) C

theorem Matroid.IsCircuit.diff_singleton_indep {α : Type u_1} {M : Matroid α} {C : Set α} {e : α} (hC : M.IsCircuit C) (he : e ∈ C) : M.Indep (C \ {e})

theorem Matroid.isCircuit_iff_forall_ssubset {α : Type u_1} {M : Matroid α} {C : Set α} : M.IsCircuit C ↔ M.Dep C ∧ ∀ ⦃I : Set α⦄, I ⊂ C → M.Indep I

theorem Matroid.isCircuit_antichain {α : Type u_1} {M : Matroid α} : IsAntichain (fun (x1 x2 : Set α) => x1 ⊆ x2) (setOf M.IsCircuit)

theorem Matroid.IsCircuit.eq_of_not_indep_subset {α : Type u_1} {M : Matroid α} {C X : Set α} (hC : M.IsCircuit C) (hX : ¬M.Indep X) (hXC : X ⊆ C) : X = C

theorem Matroid.IsCircuit.eq_of_dep_subset {α : Type u_1} {M : Matroid α} {C X : Set α} (hC : M.IsCircuit C) (hX : M.Dep X) (hXC : X ⊆ C) : X = C

theorem Matroid.IsCircuit.not_ssubset {α : Type u_1} {M : Matroid α} {C C' : Set α} (hC : M.IsCircuit C) (hC' : M.IsCircuit C') : ¬C' ⊂ C

theorem Matroid.IsCircuit.eq_of_subset_isCircuit {α : Type u_1} {M : Matroid α} {C C' : Set α} (hC : M.IsCircuit C) (hC' : M.IsCircuit C') (h : C ⊆ C') : C = C'

theorem Matroid.IsCircuit.eq_of_superset_isCircuit {α : Type u_1} {M : Matroid α} {C C' : Set α} (hC : M.IsCircuit C) (hC' : M.IsCircuit C') (h : C' ⊆ C) : C = C'

theorem Matroid.isCircuit_iff_dep_forall_diff_singleton_indep {α : Type u_1} {M : Matroid α} {C : Set α} : M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})

Independence and bases

theorem Matroid.Indep.insert_isCircuit_of_forall {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} (hI : M.Indep I) (heI : e ∉ I) (he : e ∈ M.closure I) (h : ∀ f ∈ I, e ∉ M.closure (I \ {f})) : M.IsCircuit (insert e I)

theorem Matroid.Indep.insert_isCircuit_of_forall_of_nontrivial {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} (hI : M.Indep I) (hInt : I.Nontrivial) (he : e ∈ M.closure I) (h : ∀ f ∈ I, e ∉ M.closure (I \ {f})) : M.IsCircuit (insert e I)

theorem Matroid.IsCircuit.diff_singleton_isBasis {α : Type u_1} {M : Matroid α} {C : Set α} {e : α} (hC : M.IsCircuit C) (he : e ∈ C) : M.IsBasis (C \ {e}) C

theorem Matroid.IsCircuit.isBasis_iff_eq_diff_singleton {α : Type u_1} {M : Matroid α} {C I : Set α} (hC : M.IsCircuit C) : M.IsBasis I C ↔ ∃ e ∈ C, I = C \ {e}

theorem Matroid.IsCircuit.isBasis_iff_insert_eq {α : Type u_1} {M : Matroid α} {C I : Set α} (hC : M.IsCircuit C) : M.IsBasis I C ↔ ∃ e ∈ C \ I, C = insert e I

Restriction

theorem Matroid.IsCircuit.isCircuit_restrict_of_subset {α : Type u_1} {M : Matroid α} {C R : Set α} (hC : M.IsCircuit C) (hCR : C ⊆ R) : (M.restrict R).IsCircuit C

theorem Matroid.restrict_isCircuit_iff {α : Type u_1} {M : Matroid α} {C R : Set α} (hR : R ⊆ M.E := by aesop_mat) : (M.restrict R).IsCircuit C ↔ M.IsCircuit C ∧ C ⊆ R

Fundamental IsCircuits

def Matroid.fundCircuit {α : Type u_1} (M : Matroid α) (e : α) (I : Set α) : Set α

For an independent set I and some e ∈ M.closure I \ I, M.fundCircuit e I is the unique isCircuit contained in insert e I. For the fact that this is a isCircuit, see Matroid.Indep.fundCircuit_isCircuit, and the fact that it is unique, see Matroid.IsCircuit.eq_fundCircuit_of_subset. Has the junk value {e} if e ∈ I or e ∉ M.E, and insert e I if e ∈ M.E \ M.closure I.

Equations

• M.fundCircuit e I = insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ⊆ M.closure J})

theorem Matroid.fundCircuit_eq_sInter {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} (he : e ∈ M.closure I) : M.fundCircuit e I = insert e (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J})

theorem Matroid.fundCircuit_subset_insert {α : Type u_1} (M : Matroid α) (e : α) (I : Set α) : M.fundCircuit e I ⊆ insert e I

theorem Matroid.fundCircuit_subset_ground {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} (he : e ∈ M.E) (hI : I ⊆ M.E := by aesop_mat) : M.fundCircuit e I ⊆ M.E

theorem Matroid.mem_fundCircuit {α : Type u_1} (M : Matroid α) (e : α) (I : Set α) : e ∈ M.fundCircuit e I

theorem Matroid.fundCircuit_diff_eq_inter {α : Type u_1} {I : Set α} {e : α} (M : Matroid α) (heI : e ∉ I) : M.fundCircuit e I \ {e} = M.fundCircuit e I ∩ I

theorem Matroid.fundCircuit_eq_of_mem {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (heX : e ∈ X) : M.fundCircuit e X = {e}

The fundamental isCircuit of e and X has the junk value {e} if e ∈ X

theorem Matroid.fundCircuit_eq_of_not_mem_ground {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (heX : e ∉ M.E) : M.fundCircuit e X = {e}

theorem Matroid.Indep.fundCircuit_isCircuit {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} (hI : M.Indep I) (hecl : e ∈ M.closure I) (heI : e ∉ I) : M.IsCircuit (M.fundCircuit e I)

theorem Matroid.Indep.mem_fundCircuit_iff {α : Type u_1} {M : Matroid α} {I : Set α} {e x : α} (hI : M.Indep I) (hecl : e ∈ M.closure I) (heI : e ∉ I) : x ∈ M.fundCircuit e I ↔ M.Indep (insert e I \ {x})

theorem Matroid.IsBase.fundCircuit_isCircuit {α : Type u_1} {M : Matroid α} {x : α} {B : Set α} (hB : M.IsBase B) (hxE : x ∈ M.E) (hxB : x ∉ B) : M.IsCircuit (M.fundCircuit x B)

theorem Matroid.IsCircuit.eq_fundCircuit_of_subset {α : Type u_1} {M : Matroid α} {C I : Set α} {e : α} (hC : M.IsCircuit C) (hI : M.Indep I) (hCs : C ⊆ insert e I) : C = M.fundCircuit e I

For I independent, M.fundCircuit e I is the only circuit contained in insert e I.

theorem Matroid.fundCircuit_restrict {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} {R : Set α} (hIR : I ⊆ R) (heR : e ∈ R) (hR : R ⊆ M.E) : (M.restrict R).fundCircuit e I = M.fundCircuit e I

@[simp]

theorem Matroid.fundCircuit_restrict_univ {α : Type u_1} {I : Set α} {e : α} (M : Matroid α) : (M.restrict Set.univ).fundCircuit e I = M.fundCircuit e I

Dependence

theorem Matroid.Dep.exists_isCircuit_subset {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.Dep X) : ∃ C ⊆ X, M.IsCircuit C

theorem Matroid.dep_iff_superset_isCircuit {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X ⊆ M.E := by aesop_mat) : M.Dep X ↔ ∃ C ⊆ X, M.IsCircuit C

theorem Matroid.dep_iff_superset_isCircuit' {α : Type u_1} {M : Matroid α} {X : Set α} : M.Dep X ↔ (∃ C ⊆ X, M.IsCircuit C) ∧ X ⊆ M.E

A version of Matroid.dep_iff_superset_isCircuit that has the supportedness hypothesis as part of the equivalence, rather than a hypothesis.

theorem Matroid.indep_iff_forall_subset_not_isCircuit' {α : Type u_1} {M : Matroid α} {I : Set α} : M.Indep I ↔ (∀ C ⊆ I, ¬M.IsCircuit C) ∧ I ⊆ M.E

A version of Matroid.indep_iff_forall_subset_not_isCircuit that has the supportedness hypothesis as part of the equivalence, rather than a hypothesis.

theorem Matroid.indep_iff_forall_subset_not_isCircuit {α : Type u_1} {M : Matroid α} {I : Set α} (hI : I ⊆ M.E := by aesop_mat) : M.Indep I ↔ ∀ C ⊆ I, ¬M.IsCircuit C

Closure

theorem Matroid.IsCircuit.closure_diff_singleton_eq {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) (e : α) : M.closure (C \ {e}) = M.closure C

theorem Matroid.IsCircuit.subset_closure_diff_singleton {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) (e : α) : C ⊆ M.closure (C \ {e})

theorem Matroid.IsCircuit.mem_closure_diff_singleton_of_mem {α : Type u_1} {M : Matroid α} {C : Set α} {e : α} (hC : M.IsCircuit C) (heC : e ∈ C) : e ∈ M.closure (C \ {e})

theorem Matroid.exists_isCircuit_of_mem_closure {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (he : e ∈ M.closure X) (heX : e ∉ X) : ∃ C ⊆ insert e X, M.IsCircuit C ∧ e ∈ C

theorem Matroid.mem_closure_iff_exists_isCircuit {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (he : e ∉ X) : e ∈ M.closure X ↔ ∃ C ⊆ insert e X, M.IsCircuit C ∧ e ∈ C

Extensionality

theorem Matroid.ext_isCircuit {α : Type u_1} {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E) (h : ∀ ⦃C : Set α⦄, C ⊆ M₁.E → (M₁.IsCircuit C ↔ M₂.IsCircuit C)) : M₁ = M₂

theorem Matroid.ext_isCircuit_not_indep {α : Type u_1} {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E) (h₁ : ∀ (C : Set α), M₁.IsCircuit C → ¬M₂.Indep C) (h₂ : ∀ (C : Set α), M₂.IsCircuit C → ¬M₁.Indep C) : M₁ = M₂

A stronger version of Matroid.ext_isCircuit: two matroids on the same ground set are equal if no circuit of one is independent in the other.

theorem Matroid.ext_iff_isCircuit {α : Type u_1} {M₁ M₂ : Matroid α} : M₁ = M₂ ↔ M₁.E = M₂.E ∧ ∀ (C : Set α), M₁.IsCircuit C ↔ M₂.IsCircuit C

Circuit Elimination

theorem Matroid.IsCircuit.strong_multi_elimination_insert {α : Type u_1} {M : Matroid α} {ι : Type u_2} {J : Set α} (x : ι → α) (I : ι → Set α) (z : α) (hxI : ∀ (i : ι), x i ∉ I i) (hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))) (hJx : M.IsCircuit (J ∪ Set.range x)) (hzJ : z ∈ J) (hzI : ∀ (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.

theorem Matroid.IsCircuit.strong_multi_elimination {α : Type u_1} {M : Matroid α} {ι : Type u_2} {C₀ : Set α} (hC₀ : M.IsCircuit C₀) (x : ι → α) (C : ι → Set α) (z : α) (hC : ∀ (i : ι), M.IsCircuit (C i)) (h_mem_C₀ : ∀ (i : ι), x i ∈ C₀) (h_mem : ∀ (i : ι), x i ∈ C i) (h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i') (hzC₀ : z ∈ C₀) (hzC : ∀ (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 isCircuits.

It states that, given a circuit C₀, a 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.

theorem Matroid.IsCircuit.strong_multi_elimination_set {α : Type u_1} {M : Matroid α} {C₀ : Set α} (hC₀ : M.IsCircuit C₀) (X : Set α) (S : Set (Set α)) (z : α) (hCS : ∀ C ∈ S, M.IsCircuit C) (hXC₀ : X ⊆ C₀) (hX : ∀ x ∈ X, ∃ C ∈ S, C ∩ X = {x}) (hzC₀ : z ∈ C₀) (hz : ∀ 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.

theorem Matroid.IsCircuit.strong_elimination {α : Type u_1} {M : Matroid α} {e f : α} {C₁ C₂ : Set α} (hC₁ : M.IsCircuit C₁) (hC₂ : M.IsCircuit C₂) (heC₁ : e ∈ C₁) (heC₂ : e ∈ C₂) (hfC₁ : f ∈ C₁) (hfC₂ : f ∉ C₂) : ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C ∧ f ∈ C

The strong isCircuit elimination axiom. For any pair of distinct circuits C₁, C₂ and all e ∈ C₁ ∩ C₂ and f ∈ C₁ \ C₂, there is a circuit C with f ∈ C ⊆ (C₁ ∪ C₂) \ {e}.

theorem Matroid.IsCircuit.elimination {α : Type u_1} {M : Matroid α} {C₁ C₂ : Set α} (hC₁ : M.IsCircuit C₁) (hC₂ : M.IsCircuit C₂) (h : C₁ ≠ C₂) (e : α) : ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C

The circuit elimination axiom : for any pair of distinct isCircuits C₁, C₂ and any e, some circuit is contained in (C₁ ∪ C₂) \ {e}.

This is one of the axioms when defining a finitary matroid via circuits; as an axiom, it is usually stated with the extra assumption that e ∈ C₁ ∩ C₂.

Finitary Matroids

theorem Matroid.IsCircuit.finite {α : Type u_1} {M : Matroid α} {C : Set α} [M.Finitary] (hC : M.IsCircuit C) : C.Finite

theorem Matroid.finitary_iff_forall_isCircuit_finite {α : Type u_1} {M : Matroid α} : M.Finitary ↔ ∀ (C : Set α), M.IsCircuit C → C.Finite

theorem Matroid.exists_mem_finite_closure_of_mem_closure {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} [M.Finitary] (he : e ∈ M.closure X) : ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I

In a finitary matroid, every element spanned by a set X is in fact spanned by a finite independent subset of X.

theorem Matroid.exists_subset_finite_closure_of_subset_closure {α : Type u_1} {M : Matroid α} {X Y : Set α} [M.Finitary] (hX : X.Finite) (hXY : X ⊆ M.closure Y) : ∃ I ⊆ Y, I.Finite ∧ M.Indep I ∧ X ⊆ M.closure I

In a finitary matroid, each finite set X spanned by a set Y is in fact spanned by a finite independent subset of Y.

IsCocircuits

@[reducible, inline]

abbrev Matroid.IsCocircuit {α : Type u_1} (M : Matroid α) (K : Set α) : Prop

A cocircuit is a circuit of the dual matroid, or equivalently the complement of a hyperplane.

Equations

• M.IsCocircuit K = M✶.IsCircuit K

theorem Matroid.isCocircuit_def {α : Type u_1} {M : Matroid α} {K : Set α} : M.IsCocircuit K ↔ M✶.IsCircuit K

theorem Matroid.IsCocircuit.isCircuit {α : Type u_1} {M : Matroid α} {K : Set α} (hK : M.IsCocircuit K) : M✶.IsCircuit K

theorem Matroid.IsCircuit.isCocircuit {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) : M✶.IsCocircuit C

theorem Matroid.IsCocircuit.subset_ground {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCocircuit C) : C ⊆ M.E

@[simp]

theorem Matroid.dual_isCocircuit_iff {α : Type u_1} {M : Matroid α} {C : Set α} : M✶.IsCocircuit C ↔ M.IsCircuit C

theorem Matroid.coindep_iff_forall_subset_not_isCocircuit {α : Type u_1} {M : Matroid α} {X : Set α} : M.Coindep X ↔ (∀ K ⊆ X, ¬M.IsCocircuit K) ∧ X ⊆ M.E

theorem Matroid.isCocircuit_iff_minimal {α : Type u_1} {M : Matroid α} {K : Set α} : M.IsCocircuit K ↔ Minimal (fun (X : Set α) => ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) K

A cocircuit is a minimal set that intersects every base.

theorem Matroid.isCocircuit_iff_minimal_compl_nonspanning {α : Type u_1} {M : Matroid α} {K : Set α} : M.IsCocircuit K ↔ Minimal (fun (X : Set α) => ¬M.Spanning (M.E \ X)) K

A cocircuit is a minimal set whose complement is nonspanning.

theorem Matroid.IsBase.compl_closure_diff_singleton_isCocircuit {α : Type u_1} {M : Matroid α} {e : α} {B : Set α} (hB : M.IsBase B) (he : e ∈ B) : M.IsCocircuit (M.E \ M.closure (B \ {e}))

For an element e of a base B, the complement of the closure of B \ {e} is a cocircuit.

theorem Matroid.isCocircuit_iff_minimal_compl_nonspanning' {α : Type u_1} {M : Matroid α} {K : Set α} : M.IsCocircuit K ↔ Minimal (fun (X : Set α) => ¬M.Spanning (M.E \ X) ∧ X ⊆ M.E) K

A version of cocircuit_iff_minimal_compl_nonspanning with a support assumption in the minimality

theorem Matroid.IsCircuit.inter_isCocircuit_ne_singleton {α : Type u_1} {M : Matroid α} {C : Set α} {e : α} {K : Set α} (hC : M.IsCircuit C) (hK : M.IsCocircuit K) : C ∩ K ≠ {e}

A cocircuit and a circuit cannot meet in exactly one element.

theorem Matroid.IsCircuit.isCocircuit_inter_nontrivial {α : Type u_1} {M : Matroid α} {C K : Set α} (hC : M.IsCircuit C) (hK : M.IsCocircuit K) (hCK : (C ∩ K).Nonempty) : (C ∩ K).Nontrivial

theorem Matroid.IsCircuit.isCocircuit_disjoint_or_nontrivial_inter {α : Type u_1} {M : Matroid α} {C K : Set α} (hC : M.IsCircuit C) (hK : M.IsCocircuit K) : Disjoint C K ∨ (C ∩ K).Nontrivial

theorem Matroid.dual_rankPos_iff_exists_isCircuit {α : Type u_1} {M : Matroid α} : M✶.RankPos ↔ ∃ (C : Set α), M.IsCircuit C

theorem Matroid.IsCircuit.dual_rankPos {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) : M✶.RankPos

theorem Matroid.exists_isCircuit {α : Type u_1} {M : Matroid α} [M✶.RankPos] : ∃ (C : Set α), M.IsCircuit C

theorem Matroid.rankPos_iff_exists_isCocircuit {α : Type u_1} {M : Matroid α} : M.RankPos ↔ ∃ (K : Set α), M.IsCocircuit K

def Matroid.fundCocircuit {α : Type u_1} (M : Matroid α) (e : α) (B : Set α) : Set α

The fundamental cocircuit for B and e: that is, the unique cocircuit K of M for which K ∩ B = {e}. Should be used when B is a base and e ∈ B. Has the junk value {e} if e ∉ B or e ∉ M.E.

Equations

• M.fundCocircuit e B = M✶.fundCircuit e (M✶.E \ B)

theorem Matroid.fundCocircuit_isCocircuit {α : Type u_1} {M : Matroid α} {e : α} {B : Set α} (he : e ∈ B) (hB : M.IsBase B) : M.IsCocircuit (M.fundCocircuit e B)

theorem Matroid.mem_fundCocircuit {α : Type u_1} (M : Matroid α) (e : α) (B : Set α) : e ∈ M.fundCocircuit e B

theorem Matroid.fundCocircuit_subset_insert_compl {α : Type u_1} (M : Matroid α) (e : α) (B : Set α) : M.fundCocircuit e B ⊆ insert e (M.E \ B)

theorem Matroid.fundCocircuit_inter_eq {α : Type u_1} {e : α} (M : Matroid α) {B : Set α} (he : e ∈ B) : M.fundCocircuit e B ∩ B = {e}

theorem Matroid.fundCocircuit_eq_of_not_mem_ground {α : Type u_1} {M : Matroid α} {e : α} (X : Set α) (he : e ∉ M.E) : M.fundCocircuit e X = {e}

The fundamental cocircuit of X and e has the junk value {e} if e ∉ M.E

theorem Matroid.fundCocircuit_eq_of_not_mem {α : Type u_1} {X : Set α} {e : α} (M : Matroid α) (heX : e ∉ X) : M.fundCocircuit e X = {e}

The fundamental cocircuit of X and e has the junk value {e} if e ∉ X

theorem Matroid.Indep.exists_isCocircuit_inter_eq_mem {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} (hI : M.Indep I) (heI : e ∈ I) : ∃ (K : Set α), M.IsCocircuit K ∧ K ∩ I = {e}

For every element e of an independent set I, there is a cocircuit whose intersection with I is {e}.

theorem Matroid.IsBase.mem_fundCocircuit_iff_mem_fundCircuit {α : Type u_1} {M : Matroid α} {B : Set α} {e f : α} (hB : 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.