Documentation

Mathlib.Data.Matroid.Rank.Finite

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.

source
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
Instances For
    source
    theorem Matroid.IsRkFinite.rankFinite {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.IsRkFinite X) :
    (M.restrict X).RankFinite
    source
    @[simp]
    theorem Matroid.RankFinite.isRkFinite {α : Type u_1} {M : Matroid α} [M.RankFinite] (X : Set α) :
    M.IsRkFinite X
    source
    theorem Matroid.IsBasis'.finite_iff_isRkFinite {α : Type u_1} {M : Matroid α} {X I : Set α} (hI : M.IsBasis' I X) :
    I.Finite ↔ M.IsRkFinite X
    source
    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.

    source
    theorem Matroid.IsBasis.finite_iff_isRkFinite {α : Type u_1} {M : Matroid α} {X I : Set α} (hI : M.IsBasis I X) :
    I.Finite ↔ M.IsRkFinite X
    source
    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.

    source
    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
    source
    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
    source
    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.

    source
    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
    source
    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'

    source
    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'

    source
    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'

    source
    theorem Matroid.IsRkFinite.subset {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.IsRkFinite X) (hXY : Y ⊆ X) :
    M.IsRkFinite Y
    source
    @[simp]
    theorem Matroid.isRkFinite_inter_ground_iff {α : Type u_1} {M : Matroid α} {X : Set α} :
    M.IsRkFinite (X ∩ M.E) ↔ M.IsRkFinite X
    source
    theorem Matroid.IsRkFinite.inter_ground {α : Type u_1} {M : Matroid α} {X : Set α} (h : M.IsRkFinite X) :
    M.IsRkFinite (X ∩ M.E)
    source
    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
    source
    theorem Matroid.Indep.isRkFinite_iff_finite {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) :
    M.IsRkFinite I ↔ I.Finite
    source
    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.

    source
    @[simp]
    theorem Matroid.isRkFinite_of_finite {α : Type u_1} {X : Set α} (M : Matroid α) (hX : X.Finite) :
    M.IsRkFinite X
    source
    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
    source
    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
    source
    theorem Matroid.isRkFinite_singleton {α : Type u_1} {M : Matroid α} {e : α} :
    M.IsRkFinite {e}
    source
    theorem Matroid.IsRkFinite.empty {α : Type u_1} (M : Matroid α) :
    M.IsRkFinite ∅
    source
    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
    source
    @[simp]
    theorem Matroid.isRkFinite_ground_iff_rankFinite {α : Type u_1} {M : Matroid α} :
    M.IsRkFinite M.E ↔ M.RankFinite
    source
    theorem Matroid.isRkFinite_ground {α : Type u_1} (M : Matroid α) [M.RankFinite] :
    M.IsRkFinite M.E
    source
    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
    source
    theorem Matroid.IsRkFinite.closure {α : Type u_1} {M : Matroid α} {X : Set α} (h : M.IsRkFinite X) :
    M.IsRkFinite (M.closure X)
    source
    @[simp]
    theorem Matroid.isRkFinite_closure_iff {α : Type u_1} {M : Matroid α} {X : Set α} :
    M.IsRkFinite (M.closure X) ↔ M.IsRkFinite X
    source
    theorem Matroid.IsRkFinite.union {α : Type u_1} {M : Matroid α} {X Y : Set α} (hX : M.IsRkFinite X) (hY : M.IsRkFinite Y) :
    M.IsRkFinite (X ∪ Y)
    source
    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
    source
    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
    source
    theorem Matroid.IsRkFinite.inter_right {α : Type u_1} {M : Matroid α} {X Y : Set α} (hX : M.IsRkFinite X) :
    M.IsRkFinite (X ∩ Y)
    source
    theorem Matroid.IsRkFinite.inter_left {α : Type u_1} {M : Matroid α} {X Y : Set α} (hX : M.IsRkFinite X) :
    M.IsRkFinite (Y ∩ X)
    source
    theorem Matroid.IsRkFinite.diff {α : Type u_1} {M : Matroid α} {X Y : Set α} (hX : M.IsRkFinite X) :
    M.IsRkFinite (X \ Y)
    source
    theorem Matroid.IsRkFinite.insert {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.IsRkFinite X) (e : α) :
    M.IsRkFinite (Insert.insert e X)
    source
    @[simp]
    theorem Matroid.isRkFinite_insert_iff {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} :
    M.IsRkFinite (insert e X) ↔ M.IsRkFinite X
    source
    @[simp]
    theorem Matroid.IsRkFinite.diff_singleton_iff {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} :
    M.IsRkFinite (X \ {e}) ↔ M.IsRkFinite X
    source
    theorem Matroid.isRkFinite_set {α : Type u_1} (M : Matroid α) [M.RankFinite] (X : Set α) :
    M.IsRkFinite X
    source
    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.