Structures · Combinatorics
Matroid.RankPos
A RankPos matroid is one whose bases are nonempty.
- Defined in
- Mathlib.Combinatorics.Matroid.Basic
- Shape
- One type argument · adds empty_not_isBase
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Forgetful instances
Every Matroid.RankPos is also a
Concrete types that are instances1
- Set.Elem
How is a type an instance?
Loading the hierarchy index…
Assumed by16
- Matroid.empty_not_isBase
- Matroid.IsBase.nonempty
- Matroid.exists_isCircuit
- Matroid.RankPos.empty_not_isBase
- Matroid.ground_not_isBase
- Matroid.IsBase.ssubset_ground
- Matroid.Coindep.delete_rankPos
- Matroid.instRankPosMap
- Matroid.one_le_eRank
- Matroid.exists_isNonloop
- Matroid.instRankPosMapEmbedding
- Matroid.rankPos_nonempty
- Matroid.instRankPosElemERestrictSubtype
- Matroid.isColoop_iff_forall_mem_compl_isCircuit
- Matroid.Indep.ssubset_ground
- Matroid.instRankPosMapEquiv