Structures · Combinatorics
Matroid.InvariantCardinalRank
A class stating that cardinality-valued rank is well-defined
(i.e. all bases are equicardinal) for a matroid M and its minors.
Notably, this holds for Finitary matroids; see Matroid.invariantCardinalRank_of_finitary.
- Shape
- One type argument · adds forall_card_isBasis_diff
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by27
- Matroid.IsBase.cardinalMk_eq_cRank
- Matroid.IsBasis.cardinalMk_sdiff_comm
- Matroid.IsBasis'.cardinalMk_eq_cRk
- Matroid.IsBase.cardinalMk_eq
- Matroid.IsBasis.cardinalMk_eq
- Matroid.cRk_union_closure_left_eq
- Matroid.cRk_closure_congr
- Matroid.cRk_union_closure_eq
- Matroid.IsBase.cardinalMk_sdiff_comm
- Matroid.IsBasis'.cardinalMk_sdiff_comm
- Matroid.Indep.cardinalMk_le_isBasis'
- Matroid.cRk_closure
- Matroid.cRk_union_closure_right_eq
- Matroid.Spanning.cRank_le_cardinalMk
- Matroid.IsBasis'.cardinalMk_eq
- Matroid.InvariantCardinalRank.forall_card_isBasis_diff
- Matroid.IsBasis.cardinalMk_eq_cRk
- Matroid.invariantCardinalRank_map
- Matroid.IsBasis'.cardinalMk_diff_comm
- Matroid.invariantCardinalRank_comap
- Matroid.Indep.cardinalMk_le_isBasis
- Matroid.cRk_insert_closure_eq
- Matroid.invariantCardinalRank_restrict
- Matroid.Indep.cardinalMk_le_isBase
- Matroid.IsBasis.cardinalMk_diff_comm
- Matroid.cRk_inter_add_cRk_union_le
- Matroid.IsBase.cardinalMk_diff_comm
Ancestors0
No ancestors.