Theorems · Theorem · combinatorics

Matroid.indep_iff_forall_closure_ssubset_of_ssubset

∀ {α : Type u_2} {M : Matroid α} {I : Set α},
  autoParam (I ⊆ M.E) Matroid.indep_iff_forall_closure_ssubset_of_ssubset._auto_1 →
    (M.Indep I ↔ ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I)

Defined in

Mathlib.Combinatorics.Matroid.Closure

Cited by

0 results in Mathlib

Foundations

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