Theorems · Theorem · combinatorics

Matroid.Finitary.indep_of_forall_finite

∀ {α : Type u_1} {M : Matroid α} [self : M.Finitary] (I : Set α), (∀ J ⊆ I, J.Finite → M.Indep J) → M.Indep I

I is independent if all its finite subsets are independent.

Defined in

Mathlib.Combinatorics.Matroid.Basic

Cited by

2 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

Matroid.Finitary