Theorems · Theorem · combinatorics

Matroid.exists_mem_finite_closure_of_mem_closure

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

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

Defined in

Mathlib.Combinatorics.Matroid.Circuit

Cited by

1 results in Mathlib

Foundations

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

Assumes

Matroid.Finitary