theorem Matroid.Codep.exists_isCocircuit_subset {α : Type u_1} {M : Matroid α} {D : Set α} (h : M.Codep D) : ∃ C ⊆ D, M.IsCocircuit C

theorem Matroid.IsCocircuit.codep {α : Type u_1} {M : Matroid α} {C : Set α} (h : M.IsCocircuit C) : M.Codep C

theorem Matroid.isCocircuit_iff_minimal_codep {α : Type u_1} {M : Matroid α} {C : Set α} : M.IsCocircuit C ↔ Minimal M.Codep C

theorem Matroid.codep_iff_exists_isCocircuit_subset {α : Type u_1} {M : Matroid α} {D : Set α} (hDE : D ⊆ M.E := by aesop_mat) : M.Codep D ↔ ∃ C ⊆ D, M.IsCocircuit C

theorem Matroid.exists_isCircuit_or_exists_eq_freeOn {α : Type u_1} (M : Matroid α) : (∃ (C : Set α), M.IsCircuit C) ∨ ∃ (E : Set α), M = freeOn E

theorem Matroid.exists_isCocircuit_or_exists_eq_loopyOn {α : Type u_1} (M : Matroid α) : (∃ (C : Set α), M.IsCocircuit C) ∨ ∃ (E : Set α), M = loopyOn E

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