Structures · Combinatorics
Matroid.RankFinite
A RankFinite matroid is one whose bases are finite
- Defined in
- Mathlib.Combinatorics.Matroid.Basic
- Shape
- One type argument · adds exists_finite_isBase
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Concrete types that are instances1
- Set.Elem
How is a type an instance?
Loading the hierarchy index…
Assumed by26
- Matroid.IsBase.finite
- Matroid.Indep.finite
- Matroid.RankFinite.exists_finite_isBase
- Matroid.Indep.isBase_of_cRank_le
- Matroid.not_rankInfinite
- Matroid.spanning_iff_eRk_le'
- Matroid.isRkFinite_set
- Matroid.indep_iff_eRk_eq_encard
- Matroid.Dep.eRk_lt_encard
- Matroid.Spanning.isBase_of_le_cRank
- Matroid.instRankFiniteMap
- Matroid.delete_rankFinite
- Matroid.comapOn_rankFinite
- Matroid.spanning_iff_eRk_le
- Matroid.comap_rankFinite
- Matroid.RankFinite.isRkFinite
- Matroid.instRankFiniteMapEquiv
- Matroid.IsRestriction.rankFinite
- Matroid.eRk_lt_encard_iff_dep
- Matroid.isRkFinite_ground
- Matroid.IsBasis.Finite
- Matroid.finitary_of_rankFinite
- Matroid.instRankFiniteMapEmbedding
- Matroid.instRankFiniteElemRestrictSubtype
- Matroid.contract_rankFinite
- Matroid.restrict_rankFinite