structure Matroid.IsNonspanningCircuit {α : Type u_1} (M : Matroid α) (C : Set α) : Prop

• nonspanning : M.Nonspanning C
• isCircuit : M.IsCircuit C

theorem Matroid.isNonspanningCircuit_iff {α : Type u_1} (M : Matroid α) (C : Set α) : M.IsNonspanningCircuit C ↔ M.Nonspanning C ∧ M.IsCircuit C

instance Matroid.instGroundedPredSetIsNonspanningCircuit : GroundedPred fun {α : Type u_2} => IsNonspanningCircuit

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

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

theorem Matroid.isBase_iff_forall_not_isNonspanningCircuit_subset {α : Type u_1} {M : Matroid α} [M.RankFinite] {B : Set α} (hBE : B ⊆ M.E) : M.IsBase B ↔ B.encard = M.eRank ∧ ∀ C ⊆ B, ¬M.IsNonspanningCircuit C

theorem Matroid.ext_isNonspanningCircuit {α : Type u_1} {M N : Matroid α} (hE : M.E = N.E) (hr : M.eRank = N.eRank) [M.RankFinite] (hMN : ∀ C ⊆ M.E, M.IsNonspanningCircuit C ↔ N.IsNonspanningCircuit C) : M = N

Two matroids with the same finite rank, the same ground set, and the same nonspanning circuits are equal.

theorem Matroid.isNonspanningCircuit_iff_isCircuit_encard_le {α : Type u_1} {M : Matroid α} {C : Set α} [M.RankFinite] : M.IsNonspanningCircuit C ↔ M.IsCircuit C ∧ C.encard ≤ M.eRank

theorem Matroid.ext_isCircuit_encard_le {α : Type u_1} {M N : Matroid α} (hE : M.E = N.E) (hr : M.eRank = N.eRank) [M.RankFinite] (hMN : ∀ C ⊆ M.E, C.encard ≤ M.eRank → (M.IsCircuit C ↔ N.IsCircuit C)) : M = N