Theorems · Theorem · combinatorics

Matroid.IsRkFinite.isBasis_of_subset_closure_of_subset_of_encard_le

∀ {α : Type u_1} {M : Matroid α} {I X : Set α},
  M.IsRkFinite X → X ⊆ M.closure I → I ⊆ X → I.encard ≤ M.eRk X → M.IsBasis I X

If X is a finite-rank set, and I is a subset of X of cardinality no larger than the rank of X that spans X, then I is a basis for X.

Defined in

Mathlib.Combinatorics.Matroid.Rank.ENat

Cited by

0 results in Mathlib

Foundations

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