Theorems · Theorem · combinatorics

Matroid.isBasis_iff

∀ {α : Type u_1} {M : Matroid α} {I X : Set α},
  autoParam (X ⊆ M.E) Matroid.isBasis_iff._auto_1 →
    (M.IsBasis I X ↔ M.Indep I ∧ I ⊆ X ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J)

Defined in

Mathlib.Combinatorics.Matroid.Basic

Cited by

4 results in Mathlib

Foundations

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