Structures · Combinatorics
Matroid.Finitary
A 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
- Shape
- One type argument · adds indep_of_forall_finite
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Every Matroid.Finitary is also a
Provided automatically by
Concrete types that are instances1
- Set.Elem
How is a type an instance?
Loading the hierarchy index…
Assumed by17
- Matroid.IsCircuit.finite
- Matroid.Finitary.indep_of_forall_finite
- Matroid.indep_iff_forall_finite_subset_indep
- Matroid.indep_of_forall_finite_subset_indep
- Matroid.exists_mem_finite_closure_of_mem_closure
- Matroid.comapOn_finitary
- Matroid.instFinitaryElemRestrictSubtype
- Matroid.restrict_finitary
- Matroid.instFinitaryMapEquiv
- Matroid.instFinitaryMap
- Matroid.IsRestriction.finitary
- Matroid.instFinitaryMapEmbedding
- Matroid.delete_finitary
- Matroid.exists_subset_finite_closure_of_subset_closure
- Matroid.contract_finitary
- Matroid.invariantCardinalRank_of_finitary
- Matroid.comap_finitary