Finite-rank sets

Matroid.IsRkFinite M X means that every basis of the set X in the matroid M is finite, or equivalently that the restriction of M to X is Matroid.RankFinite. Sets in a matroid with IsRkFinite are the largest class of sets for which one can do nontrivial integer arithmetic involving the rank function.

Implementation Details

Unlike most set predicates on matroids, a set X with M.IsRkFinite X need not satisfy X ⊆ M.E, so may contain junk elements. This seems to be what makes the definition easiest to use.

def Matroid.IsRkFinite {α : Type u_1} (M : Matroid α) (X : Set α) : Prop

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

Equations

• M.IsRkFinite X = (M.restrict X).RankFinite

theorem Matroid.IsRkFinite.rankFinite {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.IsRkFinite X) : (M.restrict X).RankFinite

theorem Matroid.IsBasis'.finite_iff_isRkFinite {α : Type u_1} {M : Matroid α} {X I : Set α} (hI : M.IsBasis' I X) : I.Finite ↔ M.IsRkFinite X

theorem Matroid.IsBasis'.finite_of_isRkFinite {α : Type u_1} {M : Matroid α} {X I : Set α} (hI : M.IsBasis' I X) : M.IsRkFinite X → I.Finite

Alias of the reverse direction of Matroid.IsBasis'.finite_iff_isRkFinite.

theorem Matroid.IsBasis.finite_iff_isRkFinite {α : Type u_1} {M : Matroid α} {X I : Set α} (hI : M.IsBasis I X) : I.Finite ↔ M.IsRkFinite X

theorem Matroid.IsBasis.finite_of_isRkFinite {α : Type u_1} {M : Matroid α} {X I : Set α} (hI : M.IsBasis I X) : M.IsRkFinite X → I.Finite

Alias of the reverse direction of Matroid.IsBasis.finite_iff_isRkFinite.

theorem Matroid.IsBasis'.isRkFinite_of_finite {α : Type u_1} {M : Matroid α} {X I : Set α} (hI : M.IsBasis' I X) (hIfin : I.Finite) : M.IsRkFinite X

theorem Matroid.IsBasis.isRkFinite_of_finite {α : Type u_1} {M : Matroid α} {X I : Set α} (hI : M.IsBasis I X) (hIfin : I.Finite) : M.IsRkFinite X

theorem Matroid.IsRkFinite.finite_of_isBasis' {α : Type u_1} {M : Matroid α} {X I : Set α} (h : M.IsRkFinite X) (hI : M.IsBasis' I X) : I.Finite

A basis' of an IsRkFinite set is finite.

theorem Matroid.IsRkFinite.finite_of_isBasis {α : Type u_1} {M : Matroid α} {X I : Set α} (h : M.IsRkFinite X) (hI : M.IsBasis I X) : I.Finite

theorem Matroid.IsRkFinite.exists_finite_isBasis' {α : Type u_1} {M : Matroid α} {X : Set α} (h : M.IsRkFinite X) : ∃ (I : Set α), M.IsBasis' I X ∧ I.Finite

An IsRkFinite set has a finite basis'

theorem Matroid.IsRkFinite.exists_finset_isBasis' {α : Type u_1} {M : Matroid α} {X : Set α} (h : M.IsRkFinite X) : ∃ (I : Finset α), M.IsBasis' (↑I) X

An IsRkFinite set has a finset basis'

theorem Matroid.isRkFinite_iff_exists_isBasis' {α : Type u_1} {M : Matroid α} {X : Set α} : M.IsRkFinite X ↔ ∃ (I : Set α), M.IsBasis' I X ∧ I.Finite

A set satisfies IsRkFinite iff it has a finite basis'

theorem Matroid.IsRkFinite.subset {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.IsRkFinite X) (hXY : Y ⊆ X) : M.IsRkFinite Y

@[simp]

theorem Matroid.isRkFinite_inter_ground_iff {α : Type u_1} {M : Matroid α} {X : Set α} : M.IsRkFinite (X ∩ M.E) ↔ M.IsRkFinite X

theorem Matroid.IsRkFinite.inter_ground {α : Type u_1} {M : Matroid α} {X : Set α} (h : M.IsRkFinite X) : M.IsRkFinite (X ∩ M.E)

theorem Matroid.isRkFinite_iff {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X ⊆ M.E := by aesop_mat) : M.IsRkFinite X ↔ ∃ (I : Set α), M.IsBasis I X ∧ I.Finite

theorem Matroid.Indep.isRkFinite_iff_finite {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) : M.IsRkFinite I ↔ I.Finite

theorem Matroid.Indep.finite_of_isRkFinite {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) : M.IsRkFinite I → I.Finite

Alias of the forward direction of Matroid.Indep.isRkFinite_iff_finite.

theorem Matroid.isRkFinite_of_finite {α : Type u_1} {X : Set α} (M : Matroid α) (hX : X.Finite) : M.IsRkFinite X

theorem Matroid.Indep.subset_finite_isBasis'_of_subset_of_isRkFinite {α : Type u_1} {M : Matroid α} {X I : Set α} (hI : M.Indep I) (hIX : I ⊆ X) (hX : M.IsRkFinite X) : ∃ (J : Set α), M.IsBasis' J X ∧ I ⊆ J ∧ J.Finite

theorem Matroid.Indep.subset_finite_isBasis_of_subset_of_isRkFinite {α : Type u_1} {M : Matroid α} {X I : Set α} (hI : M.Indep I) (hIX : I ⊆ X) (hX : M.IsRkFinite X) (hXE : X ⊆ M.E := by aesop_mat) : ∃ (J : Set α), M.IsBasis J X ∧ I ⊆ J ∧ J.Finite

theorem Matroid.isRkFinite_singleton {α : Type u_1} {M : Matroid α} {e : α} : M.IsRkFinite {e}

@[simp]

theorem Matroid.IsRkFinite.empty {α : Type u_1} (M : Matroid α) : M.IsRkFinite ∅

theorem Matroid.IsRkFinite.finite_of_indep_subset {α : Type u_1} {M : Matroid α} {X I : Set α} (hX : M.IsRkFinite X) (hI : M.Indep I) (hIX : I ⊆ X) : I.Finite

@[simp]

theorem Matroid.isRkFinite_ground_iff_rankFinite {α : Type u_1} {M : Matroid α} : M.IsRkFinite M.E ↔ M.RankFinite

theorem Matroid.isRkFinite_ground {α : Type u_1} (M : Matroid α) [M.RankFinite] : M.IsRkFinite M.E

theorem Matroid.Indep.finite_of_subset_isRkFinite {α : Type u_1} {M : Matroid α} {X I : Set α} (hI : M.Indep I) (hIX : I ⊆ X) (hX : M.IsRkFinite X) : I.Finite

theorem Matroid.IsRkFinite.closure {α : Type u_1} {M : Matroid α} {X : Set α} (h : M.IsRkFinite X) : M.IsRkFinite (M.closure X)

@[simp]

theorem Matroid.isRkFinite_closure_iff {α : Type u_1} {M : Matroid α} {X : Set α} : M.IsRkFinite (M.closure X) ↔ M.IsRkFinite X

theorem Matroid.IsRkFinite.union {α : Type u_1} {M : Matroid α} {X Y : Set α} (hX : M.IsRkFinite X) (hY : M.IsRkFinite Y) : M.IsRkFinite (X ∪ Y)

theorem Matroid.IsRkFinite.isRkFinite_union_iff {α : Type u_1} {M : Matroid α} {X Y : Set α} (hX : M.IsRkFinite X) : M.IsRkFinite (X ∪ Y) ↔ M.IsRkFinite Y

theorem Matroid.IsRkFinite.isRkFinite_diff_iff {α : Type u_1} {M : Matroid α} {X Y : Set α} (hX : M.IsRkFinite X) : M.IsRkFinite (Y \ X) ↔ M.IsRkFinite Y

theorem Matroid.IsRkFinite.inter_right {α : Type u_1} {M : Matroid α} {X Y : Set α} (hX : M.IsRkFinite X) : M.IsRkFinite (X ∩ Y)

theorem Matroid.IsRkFinite.inter_left {α : Type u_1} {M : Matroid α} {X Y : Set α} (hX : M.IsRkFinite X) : M.IsRkFinite (Y ∩ X)

theorem Matroid.IsRkFinite.diff {α : Type u_1} {M : Matroid α} {X Y : Set α} (hX : M.IsRkFinite X) : M.IsRkFinite (X \ Y)

theorem Matroid.IsRkFinite.insert {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.IsRkFinite X) (e : α) : M.IsRkFinite (Insert.insert e X)

@[simp]

theorem Matroid.isRkFinite_insert_iff {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} : M.IsRkFinite (insert e X) ↔ M.IsRkFinite X

@[simp]

theorem Matroid.IsRkFinite.diff_singleton_iff {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} : M.IsRkFinite (X \ {e}) ↔ M.IsRkFinite X

theorem Matroid.isRkFinite_set {α : Type u_1} (M : Matroid α) [M.RankFinite] (X : Set α) : M.IsRkFinite X

theorem Matroid.IsRkFinite.iUnion {α : Type u_1} {M : Matroid α} {ι : Type u_2} [Finite ι] {Xs : ι → Set α} (h : ∀ (i : ι), M.IsRkFinite (Xs i)) : M.IsRkFinite (⋃ (i : ι), Xs i)

A union of finitely many IsRkFinite sets is IsRkFinite.