Theorems · Inductive type · combinatorics
Matroid.Finitary
{α : Type u_1} → Matroid α → PropA Finitary matroid is one where a set is independent if and only if it all
its finite subsets are independent, or equivalently a matroid whose circuits are finite.
- Defined in
- Mathlib.Combinatorics.Matroid.Basic
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Matroidstatement · cited by 1,258
Cited by13
Results whose statement or proof uses this declaration.
- Matroid.Finitary.indep_of_forall_finitestatement and proof · cited by 2
- Matroid.IsCircuit.finitestatement and proof · cited by 2
- Matroid.exists_mem_finite_closure_of_mem_closurestatement and proof · cited by 1
- Matroid.indep_iff_forall_finite_subset_indepstatement and proof · cited by 1
- Matroid.Finitary.casesOnstatement and proof · cited by 1
- Matroid.Finitary.sigmastatement and proof · cited by 1
- Matroid.indep_of_forall_finite_subset_indepstatement and proof · cited by 1
- Matroid.exists_subset_finite_closure_of_subset_closurestatement and proof · cited by 0
- Matroid.finitary_iffstatement and proof · cited by 0
- Matroid.finitary_iff_forall_isCircuit_finitestatement and proof · cited by 0
- Matroid.Finitary.recOnstatement and proof · cited by 0
- Matroid.Finitary.sum'statement and proof · cited by 0