Documentation

Matroid.Rank.ENat

instance Matroid.instInvariantFunSetENatERk :

InvariantFun (fun {α : Type u_3} => eRk) fun {β : Type u_4} => eRk

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

M.eRk X ≤ M.eRk Y

theorem Matroid.spanning_iff_eRk' {α : Type u_1} {M : Matroid α} {X : Set α} [M.RankFinite] :

M.Spanning X ↔ M.eRank ≤ M.eRk X ∧ X ⊆ M.E

theorem Matroid.spanning_iff_eRk {α : Type u_1} {M : Matroid α} {X : Set α} [M.RankFinite] (hX : X ⊆ M.E := by aesop_mat) :

M.Spanning X ↔ M.eRank ≤ M.eRk X

theorem Matroid.Nonspanning.eRk_add_one_le {α : Type u_1} {M : Matroid α} {X : Set α} (h : M.Nonspanning X) :

M.eRk X + 1 ≤ M.eRank

theorem Matroid.IsLoopEquiv.eRk_eq_eRk {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.IsLoopEquiv X Y) :

M.eRk X = M.eRk Y

@[simp]

theorem Matroid.eRank_lt_top {α : Type u_1} {M : Matroid α} [M.RankFinite] :

@[simp]

theorem Matroid.eRk_lt_top {α : Type u_1} {M : Matroid α} [M.RankFinite] {X : Set α} :

@[simp]

theorem Matroid.eRk_ne_top {α : Type u_1} {M : Matroid α} [M.RankFinite] {X : Set α} :

M.eRk X ≠ ⊤

theorem Matroid.Nonspanning.eRk_lt {α : Type u_1} {M : Matroid α} {X : Set α} [M.RankFinite] (h : M.Nonspanning X) :

M.eRk X < M.eRank

theorem Matroid.nonspanning_iff_eRk_lt {α : Type u_1} {M : Matroid α} {X : Set α} [M.RankFinite] (hXE : X ⊆ M.E := by aesop_mat) :

M.Nonspanning X ↔ M.eRk X < M.eRank

theorem Matroid.nonspanning_of_eRk_ne {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.eRk X ≠ M.eRank) (hXE : X ⊆ M.E := by aesop_mat) :

M.Nonspanning X

theorem Matroid.eRank_pos {α : Type u_1} (M : Matroid α) [M.RankPos] :

theorem Matroid.eRank_ne_zero {α : Type u_1} (M : Matroid α) [M.RankPos] :

theorem Matroid.eRank_ne_zero_iff {α : Type u_1} (M : Matroid α) :

M.eRank ≠ 0 ↔ M.RankPos

instance Matroid.instRankPosOfRankInfinite_matroid {α : Type u_1} {M : Matroid α} [M.RankInfinite] :

@[simp]

theorem Matroid.rankPos_restrict_iff {α : Type u_1} {M : Matroid α} {X : Set α} :

(M.restrict X).RankPos ↔ M.eRk X ≠ 0

theorem Matroid.Dep.eRk_add_one_le_encard {α : Type u_1} {M : Matroid α} {X : Set α} (h : M.Dep X) :

M.eRk X + 1 ≤ X.encard

theorem Matroid.IsNonloop.subset_closure_of_eRk_le_one {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (he : M.IsNonloop e) (hX : M.eRk X ≤ 1) (heX : e ∈ X) (hXE : X ⊆ M.E := by aesop_mat) :

X ⊆ M.closure {e}

@[simp]

theorem Matroid.disjointSum_eRk_eq {α : Type u_1} (M N : Matroid α) (hMN : Disjoint M.E N.E) (X : Set α) :

(M.disjointSum N hMN).eRk X = M.eRk (X ∩ M.E) + N.eRk (X ∩ N.E)

@[simp]

theorem Matroid.disjointSum_eRank_eq {α : Type u_1} (M N : Matroid α) (hMN : Disjoint M.E N.E) :

(M.disjointSum N hMN).eRank = M.eRank + N.eRank

theorem Matroid.eRk_eq_iSup_finset_eRk {α : Type u_1} (M : Matroid α) (X : Set α) :

M.eRk X = ⨆ Y ∈ {S : Finset α | ↑S ⊆ X}, M.eRk ↑Y

theorem Matroid.eRk_union_eq_of_subset_of_eRk_le_eRk {α : Type u_1} {M : Matroid α} {X Y : Set α} (Z : Set α) (hXY : X ⊆ Y) (hr : M.eRk Y ≤ M.eRk X) :

M.eRk (X ∪ Z) = M.eRk (Y ∪ Z)

theorem Matroid.eRk_union_eq_of_subsets_of_eRks_le {α : Type u_1} {M : Matroid α} {X X' Y Y' : Set α} (hX : X ⊆ X') (hY : Y ⊆ Y') (hXX' : M.eRk X' ≤ M.eRk X) (hYY' : M.eRk Y' ≤ M.eRk Y) :

M.eRk (X ∪ Y) = M.eRk (X' ∪ Y')

theorem Matroid.not_isRkFinite_of_eRk_ge {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : ¬M.IsRkFinite X) (hXY : M.eRk X ≤ M.eRk Y) :

¬M.IsRkFinite Y

theorem Matroid.eRk_restrict {α : Type u_1} (M : Matroid α) (R X : Set α) :

(M.restrict R).eRk X = M.eRk (X ∩ R)

@[simp]

theorem Matroid.eRk_restrict_univ {α : Type u_1} (M : Matroid α) (X : Set α) :

(M.restrict Set.univ).eRk X = M.eRk X

theorem Matroid.IsRestriction.eRk_eq {α : Type u_1} {M N : Matroid α} (h : N.IsRestriction M) {X : Set α} (hX : X ⊆ N.E) :

N.eRk X = M.eRk X

theorem Matroid.IsSpanningRestriction.eRank_eq {α : Type u_1} {M N : Matroid α} (h : N.IsSpanningRestriction M) :

N.eRank = M.eRank

theorem Matroid.eRank_comapOn {α : Type u_1} {β : Type u_3} {M : Matroid β} {E : Set α} (f : α → β) (hM : Set.SurjOn f E M.E) :

(M.comapOn E f).eRank = M.eRank

theorem Matroid.eRank_comap {α : Type u_1} {β : Type u_3} {M : Matroid β} (f : α → β) (hM : M.E ⊆ Set.range f) :

(M.comap f).eRank = M.eRank

def Matroid.RkLE {α : Type u_1} (M : Matroid α) (k : ℕ∞) (X : Set α) :

The property of having rank at most k in a matroid M.

Equations

M.RkLE k X = (M.eRk X ≤ k)

Instances For

theorem Matroid.RkLE.le {α : Type u_1} {M : Matroid α} {X : Set α} {k : ℕ∞} (h : M.RkLE k X) :

M.eRk X ≤ k

theorem Matroid.rkLE_self {α : Type u_1} (M : Matroid α) (X : Set α) :

M.RkLE (M.eRk X) X

@[simp]

theorem Matroid.rkLE_empty {α : Type u_1} {M : Matroid α} {k : ℕ∞} :

@[simp]

theorem Matroid.rkLE_singleton {α : Type u_1} {M : Matroid α} {e : α} :

M.RkLE 1 {e}

theorem Matroid.RkLE.mono {α : Type u_1} {M : Matroid α} {X : Set α} {l k : ℕ∞} (h : M.RkLE l X) (hlk : l ≤ k) :

M.RkLE k X

theorem Matroid.rkLE_eRank {α : Type u_1} (M : Matroid α) (X : Set α) :

M.RkLE M.eRank X

theorem Matroid.RkLE.subset {α : Type u_1} {M : Matroid α} {X Y : Set α} {k : ℕ∞} (h : M.RkLE k X) (hYX : Y ⊆ X) :

M.RkLE k Y

@[simp]

theorem Matroid.antitone_rkLE {α : Type u_1} {M : Matroid α} {k : ℕ∞} :

Antitone (M.RkLE k)

theorem Matroid.RkLE.closure {α : Type u_1} {M : Matroid α} {X : Set α} {k : ℕ∞} (h : M.RkLE k X) :

M.RkLE k (M.closure X)

@[simp]

theorem Matroid.rkLE_closure_iff {α : Type u_1} {M : Matroid α} {X : Set α} {k : ℕ∞} :

M.RkLE k (M.closure X) ↔ M.RkLE k X

theorem Matroid.eRk_insert_of_mem_closure {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (he : e ∈ M.closure X) :

M.eRk (insert e X) = M.eRk X

theorem Matroid.IsRkFinite.mem_closure_iff {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (h : M.IsRkFinite X) (he : e ∈ M.E := by aesop_mat) :

e ∈ M.closure X ↔ M.eRk (Insert.insert e X) = M.eRk X

theorem Matroid.IsRkFinite.mem_closure_iff_le {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (h : M.IsRkFinite X) (he : e ∈ M.E := by aesop_mat) :

e ∈ M.closure X ↔ M.eRk (Insert.insert e X) ≤ M.eRk X