Mathlib Map

Theorems · Definition · combinatorics

Matroid.IsRkFinite

{α : Type u_1} → Matroid α → Set α → Prop

Matroid.IsRkFinite M X means that every basis of X in M is finite.

Defined in
Mathlib.Combinatorics.Matroid.Rank.Finite
Cited by
53 results in Mathlib
Foundations
Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Matroid.IsRkFinite.subset · cited by 10IsRkFinite.subsetMatroid.IsBasis'.isRkFinite_of_finite · cited by 5IsBasis'.isRkFinite_of_fi…Matroid.isRkFinite_inter_ground_iff · cited by 4Matroid.isRkFinite_inter_…Matroid.IsRkFinite.closure · cited by 3IsRkFinite.closureMatroid.IsRkFinite.eRk_lt_top · cited by 3IsRkFinite.eRk_lt_topMatroid.IsRkFinite.exists_finite_isBasis' · cited by 3IsRkFinite.exists_finite_…Matroid.isRkFinite_of_finite · cited by 3Matroid.isRkFinite_of_fin…Matroid.isRkFinite_singleton · cited by 3Matroid.isRkFinite_single…Matroid.IsBasis'.finite_iff_isRkFinite · cited by 3IsBasis'.finite_iff_isRkF…Matroid.IsBasis'.finite_of_isRkFinite · cited by 3IsBasis'.finite_of_isRkFi…Matroid.IsBasis.finite_iff_isRkFinite · cited by 2IsBasis.finite_iff_isRkFi…Matroid.IsBasis.finite_of_isRkFinite · cited by 2IsBasis.finite_of_isRkFin…Matroid.IsRkFinite.isRkFinite_sdiff_iff · cited by 2IsRkFinite.isRkFinite_sdi…Matroid.IsRkFinite.isRkFinite_union_iff · cited by 2IsRkFinite.isRkFinite_uni…Matroid.IsRkFinite.finite_of_isBasis' · cited by 2IsRkFinite.finite_of_isBa…Set · cited by 53352SetMatroid · cited by 1258MatroidMatroid.restrict · cited by 111Matroid.restrictMatroid.RankFinite · cited by 33Matroid.RankFiniteMatroid.IsRkFiniteCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by53

Results whose statement or proof uses this declaration.