Theorems · Theorem · combinatorics

Matroid.exists_subset_finite_closure_of_subset_closure

∀ {α : Type u_1} {M : Matroid α} {X Y : Set α} [M.Finitary],
  X.Finite → X ⊆ M.closure Y → ∃ I ⊆ Y, I.Finite ∧ M.Indep I ∧ X ⊆ M.closure I

In a finitary matroid, each finite set X spanned by a set Y is in fact spanned by a finite independent subset of Y.

Defined in

Mathlib.Combinatorics.Matroid.Circuit

Cited by

0 results in Mathlib

Foundations

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

Assumes

Matroid.Finitary