A Circuit of a matroid is a minimal dependent set.

theorem Matroid.IsBasis.switch_subset_of_isBasis_closure {α : Type u_1} {M : Matroid α} {I X I₀ J₀ : Set α} (hIX : M.IsBasis I X) (hI₀ : I₀ ⊆ I) (hJ₀X : J₀ ⊆ X) (hJ₀ : M.IsBasis J₀ (M.closure I₀)) : M.IsBasis (I \ I₀ ∪ J₀) X

theorem Matroid.IsCocircuit.finite {α : Type u_1} {M : Matroid α} {K : Set α} [M✶.Finitary] (hK : M.IsCocircuit K) : K.Finite

theorem Matroid.IsCircuit.exists_mem_of_mem_isCocircuit {α : Type u_1} {M : Matroid α} {C K : Set α} {e : α} (hC : M.IsCircuit C) (hK : M.IsCocircuit K) (heC : e ∈ C) (heK : e ∈ K) : ∃ f ∈ C, f ∈ K ∧ f ≠ e

def Matroid.Cyclic {α : Type u_1} (M : Matroid α) (A : Set α) : Prop

A cyclic set is a (possibly empty) union of circuits. This is the same as a complement of a flat in the dual matroid, and a number of other conditions; see Matroid.cyclic_tfae.

Equations

• M.Cyclic A = ∃ (Cs : Set (Set α)), A = ⋃₀ Cs ∧ ∀ C ∈ Cs, M.IsCircuit C

theorem Matroid.Cyclic.exists {α : Type u_1} {M : Matroid α} {A : Set α} (hA : M.Cyclic A) : ∃ (Cs : Set (Set α)), A = ⋃₀ Cs ∧ ∀ C ∈ Cs, M.IsCircuit C

theorem Matroid.Cyclic.subset_ground {α : Type u_1} {M : Matroid α} {A : Set α} (hA : M.Cyclic A) : A ⊆ M.E

@[simp]

theorem Matroid.empty_cyclic {α : Type u_1} (M : Matroid α) : M.Cyclic ∅

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

theorem Matroid.Cyclic.exists_of_mem {α : Type u_1} {M : Matroid α} {e : α} {A : Set α} (hA : M.Cyclic A) (he : e ∈ A) : ∃ C ⊆ A, M.IsCircuit C ∧ e ∈ C

theorem Matroid.Cyclic.dep_of_nonempty {α : Type u_1} {M : Matroid α} {A : Set α} (hA : M.Cyclic A) : A.Nonempty → M.Dep A

theorem Matroid.Cyclic.eq_sUnion {α : Type u_1} {M : Matroid α} {A : Set α} (hA : M.Cyclic A) : A = ⋃₀ {C : Set α | M.IsCircuit C ∧ C ⊆ A}

theorem Matroid.cyclic_iff_forall_exists {α : Type u_1} {M : Matroid α} {A : Set α} : M.Cyclic A ↔ ∀ e ∈ A, ∃ C ⊆ A, M.IsCircuit C ∧ e ∈ C

theorem Matroid.dual_cyclic_iff {α : Type u_1} {M : Matroid α} {A : Set α} (hA : A ⊆ M.E := by aesop_mat) : M✶.Cyclic A ↔ M.IsFlat (M.E \ A)

theorem Matroid.dual_cyclic_iff' {α : Type u_1} {M : Matroid α} {A : Set α} : M✶.Cyclic A ↔ M.IsFlat (M.E \ A) ∧ A ⊆ M.E

A version of Matroid.dual_cyclic_iff where the supportedness assumption is part of the equivalence rather than the hypothesis.

theorem Matroid.cyclic_iff_compl_isFlat_dual {α : Type u_1} {M : Matroid α} {A : Set α} (hA : A ⊆ M.E := by aesop_mat) : M.Cyclic A ↔ M✶.IsFlat (M.E \ A)

theorem Matroid.cyclic_iff_compl_isFlat_dual' {α : Type u_1} {M : Matroid α} {A : Set α} : M.Cyclic A ↔ M✶.IsFlat (M.E \ A) ∧ A ⊆ M.E

theorem Matroid.Cyclic.compl_isFlat_dual {α : Type u_1} {M : Matroid α} {A : Set α} (hA : M.Cyclic A) : M✶.IsFlat (M.E \ A)

theorem Matroid.compl_cyclic_iff {α : Type u_1} {M : Matroid α} {A : Set α} (hAE : A ⊆ M.E := by aesop_mat) : M.Cyclic (M.E \ A) ↔ M✶.IsFlat A

theorem Matroid.compl_cyclic_dual_iff {α : Type u_1} {M : Matroid α} {F : Set α} (hF : F ⊆ M.E := by aesop_mat) : M✶.Cyclic (M.E \ F) ↔ M.IsFlat F

theorem Matroid.IsFlat.compl_cyclic_dual {α : Type u_1} {M : Matroid α} {F : Set α} (hF : M.IsFlat F) : M✶.Cyclic (M.E \ F)

theorem Matroid.isFlat_dual_iff_compl_cyclic {α : Type u_1} {M : Matroid α} {F : Set α} (hF : F ⊆ M.E := by aesop_mat) : M✶.IsFlat F ↔ M.Cyclic (M.E \ F)

theorem Matroid.cyclic_tfae {α : Type u_1} {M : Matroid α} {A : Set α} : [M.Cyclic A, ∃ (Cs : Set (Set α)), A = ⋃₀ Cs ∧ ∀ C ∈ Cs, M.IsCircuit C, ∀ e ∈ A, ∃ C ⊆ A, M.IsCircuit C ∧ e ∈ C, ∀ e ∈ A, e ∈ M.closure (A \ {e}), (∀ (K : Set α), M.IsCocircuit K → (A ∩ K).encard ≠ 1) ∧ A ⊆ M.E, M✶.IsFlat (M.E \ A) ∧ A ⊆ M.E].TFAE

theorem Matroid.cyclic_iff_forall_inter_isCocircuit_encard_ne {α : Type u_1} {M : Matroid α} {A : Set α} (hAE : A ⊆ M.E := by aesop_mat) : M.Cyclic A ↔ ∀ (K : Set α), M.IsCocircuit K → (A ∩ K).encard ≠ 1

theorem Matroid.cyclic_iff_forall_mem_closure_diff_singleton {α : Type u_1} {M : Matroid α} {A : Set α} : M.Cyclic A ↔ ∀ e ∈ A, e ∈ M.closure (A \ {e})

theorem Matroid.Cyclic.iUnion {α : Type u_1} {M : Matroid α} {ι : Type u_2} (As : ι → Set α) (hAs : ∀ (i : ι), M.Cyclic (As i)) : M.Cyclic (⋃ (i : ι), As i)

theorem Matroid.Cyclic.sUnion {α : Type u_1} {M : Matroid α} (As : Set (Set α)) (hAs : ∀ A ∈ As, M.Cyclic A) : M.Cyclic (⋃₀ As)

theorem Matroid.Cyclic.biUnion {α : Type u_1} {M : Matroid α} {ι : Type u_2} {As : ι → Set α} {I : Set ι} (hAs : ∀ i ∈ I, M.Cyclic (As i)) : M.Cyclic (⋃ i ∈ I, As i)

theorem Matroid.Cyclic.union {α : Type u_1} {M : Matroid α} {A B : Set α} (hA : M.Cyclic A) (hB : M.Cyclic B) : M.Cyclic (A ∪ B)

theorem Matroid.Cyclic.restrict {α : Type u_1} {M : Matroid α} {R A : Set α} (hA : M.Cyclic A) (hAR : A ⊆ R) : (M.restrict R).Cyclic A

theorem Matroid.Cyclic.of_restrict {α : Type u_1} {M : Matroid α} {A R : Set α} (hA : (M.restrict R).Cyclic A) (hR : R ⊆ M.E := by aesop_mat) : M.Cyclic A

theorem Matroid.restrict_cyclic_iff {α : Type u_1} {M : Matroid α} {A : Set α} (R : Set α) (hR : R ⊆ M.E := by aesop_mat) : (M.restrict R).Cyclic A ↔ M.Cyclic A ∧ A ⊆ R

theorem Matroid.Cyclic.eq_biUnion_fundCircuits {α : Type u_1} {M : Matroid α} {I A : Set α} (hA : M.Cyclic A) (hI : M.IsBasis I A) : A = ⋃ e ∈ A \ I, M.fundCircuit e I

A cyclic set is the union of its fundamental circuits for some basis.

theorem Matroid.Cyclic.exists_eq_union_isCircuit_cyclic_ssubset {α : Type u_1} {M : Matroid α} {A : Set α} (hA : M.Cyclic A) (hne : A.Nonempty) : ∃ (C : Set α) (A₀ : Set α), C ⊆ A ∧ A₀ ⊂ A ∧ M.IsCircuit C ∧ M.Cyclic A₀ ∧ C ∪ A₀ = A

Every nonempty cyclic set is the union of a circuit and a smaller cyclic set. This can be used for induction.

theorem Matroid.minimal_nonempty_cyclic_iff_isCircuit {α : Type u_1} {M : Matroid α} {C : Set α} : Minimal (fun (A : Set α) => M.Cyclic A ∧ A.Nonempty) C ↔ M.IsCircuit C

A minimal nonempty cyclic set is a circuit.

theorem Matroid.mem_closure_iff_mem_or_exists_isCircuit {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (hX : X ⊆ M.E := by aesop_mat) : e ∈ M.closure X ↔ e ∈ X ∨ ∃ C ⊆ insert e X, M.IsCircuit C ∧ e ∈ C

instance Matroid.instGroundedPredSetIsCircuit : GroundedPred fun {α : Type u_2} => IsCircuit

instance Matroid.instGroundedPredSetIsCocircuit : GroundedPred fun {α : Type u_2} => IsCocircuit

instance Matroid.instInvariantFunSetPropIsCircuit : InvariantFun (fun {α : Type u_2} => IsCircuit) fun {β : Type u_3} => IsCircuit

instance Matroid.instInvariantFunSetPropIsCocircuit : InvariantFun (fun {α : Type u_2} => IsCocircuit) fun {β : Type u_3} => IsCocircuit

theorem Matroid.map_isCircuit_iff {α : Type u_1} {M : Matroid α} {β : Type u_2} {C : Set β} (f : α → β) (hf : Set.InjOn f M.E) : (M.map f hf).IsCircuit C ↔ ∃ (C₀ : Set α), M.IsCircuit C₀ ∧ C = f '' C₀

theorem Matroid.mapEquiv_isCircuit_iff {α : Type u_1} {M : Matroid α} {β : Type u_2} {C : Set β} (f : α ≃ β) : (M.mapEquiv f).IsCircuit C ↔ M.IsCircuit (⇑f.symm '' C)

theorem Matroid.map_isCocircuit_iff {α : Type u_1} {M : Matroid α} {β : Type u_2} {C : Set β} (f : α → β) (hf : Set.InjOn f M.E) : (M.map f hf).IsCocircuit C ↔ ∃ (C₀ : Set α), M.IsCocircuit C₀ ∧ C = f '' C₀

@[simp]

theorem Matroid.restrictSubtype_ground_isCircuit_iff {α : Type u_1} {M : Matroid α} {C : Set ↑M.E} : (M.restrictSubtype M.E).IsCircuit C ↔ M.IsCircuit (Subtype.val '' C)

@[simp]

theorem Matroid.uniqueBaseOn_dep_iff {α : Type u_1} {I E D : Set α} : (uniqueBaseOn I E).Dep D ↔ D.Nonempty ∧ ¬D ⊆ I ∧ D ⊆ E

@[simp]

theorem Matroid.loopyOn_dep_iff {α : Type u_1} {E D : Set α} : (loopyOn E).Dep D ↔ D.Nonempty ∧ D ⊆ E

@[simp]

theorem Matroid.uniqueBaseOn_isCircuit_iff {α : Type u_1} {C I E : Set α} : (uniqueBaseOn I E).IsCircuit C ↔ ∃ e ∈ E \ I, C = {e}

@[simp]

theorem Matroid.freeOn_not_isCircuit {α : Type u_1} {C E : Set α} : ¬(freeOn E).IsCircuit C

@[simp]

theorem Matroid.loopyOn_isCircuit_iff {α : Type u_1} {C E : Set α} : (loopyOn E).IsCircuit C ↔ ∃ e ∈ E, C = {e}

@[simp]

theorem Matroid.emptyOn_not_isCircuit {α : Type u_1} {C : Set α} : ¬(emptyOn α).IsCircuit C

theorem Matroid.IsCircuit.of_isRestriction {α : Type u_1} {M : Matroid α} {C : Set α} {N : Matroid α} (hC : N.IsCircuit C) (hNM : N.IsRestriction M) : M.IsCircuit C

noncomputable def Matroid.girth {α : Type u_1} (M : Matroid α) : ℕ∞

The girth of M is the cardinality of the smallest circuit of M, or ⊤ if none exists.

Equations

• M.girth = ⨅ C ∈ {C : Set α | M.IsCircuit C}, C.encard

theorem Matroid.one_le_girth {α : Type u_1} (M : Matroid α) : 1 ≤ M.girth

theorem Matroid.IsCircuit.girth_le_card {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) : M.girth ≤ C.encard

theorem Matroid.girth_eq_top_iff {α : Type u_1} {M : Matroid α} : M.girth = ⊤ ↔ ∀ (C : Set α), M.IsCircuit C → C.Infinite

@[simp]

theorem Matroid.girth_eq_top_iff_ground_indep {α : Type u_1} {M : Matroid α} [M.Finitary] : M.girth = ⊤ ↔ M = freeOn M.E

theorem Matroid.le_girth_iff {α : Type u_1} {M : Matroid α} {k : ℕ∞} : k ≤ M.girth ↔ ∀ (C : Set α), M.IsCircuit C → k ≤ C.encard

theorem Matroid.exists_isCircuit_girth {α : Type u_1} (M : Matroid α) [M✶.RankPos] : ∃ (C : Set α), M.IsCircuit C ∧ C.encard = M.girth

theorem Matroid.girth_le_eRank_add_one {α : Type u_1} (M : Matroid α) [M✶.RankPos] : M.girth ≤ M.eRank + 1

@[simp]

theorem Matroid.girth_emptyOn {α : Type u_1} : (emptyOn α).girth = ⊤

@[simp]

theorem Matroid.girth_freeOn {α : Type u_1} {E : Set α} : (freeOn E).girth = ⊤

theorem Matroid.girth_le_iff {α : Type u_1} {M : Matroid α} {k : ℕ∞} [M✶.RankPos] : M.girth ≤ k ↔ ∃ (C : Set α), M.IsCircuit C ∧ C.encard ≤ k

theorem Matroid.girth_le_iff' {α : Type u_1} {M : Matroid α} {k : ℕ} : M.girth ≤ ↑k ↔ ∃ (C : Finset α), M.IsCircuit ↑C ∧ C.card ≤ k

theorem Matroid.girth_loopyOn {α : Type u_1} {E : Set α} (hE : E.Nonempty) : (loopyOn E).girth = 1

theorem Matroid.girth_lt_iff {α : Type u_1} {M : Matroid α} {k : ℕ∞} : M.girth < k ↔ ∃ (C : Set α), M.IsCircuit C ∧ C.encard < k

theorem Matroid.lt_girth_iff {α : Type u_1} {M : Matroid α} {k : ℕ∞} [M✶.RankPos] : k < M.girth ↔ ∀ (C : Set α), M.IsCircuit C → k < C.encard

theorem Matroid.lt_girth_iff' {α : Type u_1} {M : Matroid α} {k : ℕ} : ↑k < M.girth ↔ ∀ (C : Finset α), M.IsCircuit ↑C → k < C.card

theorem Matroid.indep_of_card_lt_girth {α : Type u_1} {M : Matroid α} {I : Set α} (hI : I.encard < M.girth) (hIE : I ⊆ M.E := by aesop_mat) : M.Indep I

theorem Matroid.indep_of_eRk_add_one_lt_girth {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.eRk I + 1 < M.girth) (hIE : I ⊆ M.E := by aesop_mat) : M.Indep I

theorem Matroid.IsRestriction.girth_ge {α : Type u_1} {N M : Matroid α} (h : N.IsRestriction M) : M.girth ≤ N.girth

theorem Matroid.girth_le_girth_restrict {α : Type u_1} {R : Set α} (M : Matroid α) (hR : R ⊆ M.E) : M.girth ≤ (M.restrict R).girth

theorem Matroid.Dep.isCircuit_of_encard_le_girth {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.Dep X) (hXfin : X.Finite) (hXcard : X.encard ≤ M.girth) : M.IsCircuit X

theorem Matroid.Dep.isCircuit_of_encard_lt_girth_add_one {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.Dep X) (hXcard : X.encard < M.girth + 1) : M.IsCircuit X

theorem Matroid.Dep.girth_le_card {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.Dep X) : M.girth ≤ X.encard

theorem Matroid.Dep.girth_le_eRk_add_one {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.Dep X) : M.girth ≤ M.eRk X + 1

theorem Matroid.IsBase.strong_exchange {α : Type u_1} {M : Matroid α} {e : α} {B₁ B₂ : Set α} (hB₁ : M.IsBase B₁) (hB₂ : M.IsBase B₂) (he : e ∈ B₁ \ B₂) : ∃ f ∈ B₂ \ B₁, M.IsBase (insert e B₂ \ {f}) ∧ M.IsBase (insert f B₁ \ {e})

theorem Matroid.IsBasis.strong_exchange {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} {I₁ I₂ : Set α} (hI₁ : M.IsBasis I₁ X) (hI₂ : M.IsBasis I₂ X) (he : e ∈ I₁ \ I₂) : ∃ f ∈ I₂ \ I₁, M.IsBasis (insert e I₂ \ {f}) X ∧ M.IsBasis (insert f I₁ \ {e}) X

theorem Matroid.IsBase.rev_exchange {α : Type u_1} {M : Matroid α} {e : α} {B₁ B₂ : Set α} (hB₁ : M.IsBase B₁) (hB₂ : M.IsBase B₂) (he : e ∈ B₁ \ B₂) : ∃ f ∈ B₂ \ B₁, M.IsBase (insert e B₂ \ {f})

theorem Matroid.IsBasis.rev_exchange {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} {I₁ I₂ : Set α} (hI₁ : M.IsBasis I₁ X) (hI₂ : M.IsBasis I₂ X) (he : e ∈ I₁ \ I₂) : ∃ f ∈ I₂ \ I₁, M.IsBasis (insert e I₂ \ {f}) X

theorem Matroid.sigma_isCircuit_iff {ι : Type u_2} {α : ι → Type u_3} (M : (i : ι) → Matroid (α i)) {C : Set ((i : ι) × α i)} : (Matroid.sigma M).IsCircuit C ↔ ∃ (i : ι) (C₀ : Set (α i)), (M i).IsCircuit C₀ ∧ C = Sigma.mk i '' C₀

theorem Matroid.sigma_isCircuit_iff' {ι : Type u_2} {α : ι → Type u_3} (M : (i : ι) → Matroid (α i)) {C : Set ((i : ι) × α i)} : (Matroid.sigma M).IsCircuit C ↔ ∃ (i : ι), C ⊆ Set.range (Sigma.mk i) ∧ (M i).IsCircuit (Sigma.mk i ⁻¹' C)

@[simp]

theorem Matroid.disjointSigma_isCircuit_iff {α : Type u_4} {ι : Type u_5} {M : ι → Matroid α} (hdj : Pairwise (Function.onFun Disjoint fun (i : ι) => (M i).E)) {C : Set α} : (Matroid.disjointSigma M hdj).IsCircuit C ↔ ∃ (i : ι), (M i).IsCircuit C

theorem Matroid.sum_isCircuit_iff {α : Type u_4} {β : Type u_5} (M : Matroid α) (N : Matroid β) {C : Set (α ⊕ β)} : (M.sum N).IsCircuit C ↔ C ⊆ Set.range Sum.inl ∧ M.IsCircuit (Sum.inl ⁻¹' C) ∨ C ⊆ Set.range Sum.inr ∧ N.IsCircuit (Sum.inr ⁻¹' C)

@[simp]

theorem Matroid.disjointSum_isCircuit_iff {α : Type u_4} {M N : Matroid α} (hdj : Disjoint M.E N.E) {C : Set α} : (M.disjointSum N hdj).IsCircuit C ↔ M.IsCircuit C ∨ N.IsCircuit C

theorem Matroid.restrict_isCircuit_iff' {α : Type u_1} {M : Matroid α} {R C : Set α} : (M.restrict R).IsCircuit C ↔ M.IsCircuit C ∧ C ⊆ R ∨ ∃ e ∈ R \ M.E, C = {e}