@[simp]

theorem Matroid.delete_eRk_eq' {α : Type u_1} (M : Matroid α) (D X : Set α) : (M.delete D).eRk X = M.eRk (X \ D)

theorem Matroid.delete_eRk_eq {α : Type u_1} {D X : Set α} (M : Matroid α) (h : Disjoint X D) : (M.delete D).eRk X = M.eRk X

theorem Matroid.delete_eRk_eq_delete_eRk_diff {α : Type u_1} (M : Matroid α) (D X : Set α) : (M.delete D).eRk X = (M.delete D).eRk (X \ D)

@[simp]

theorem Matroid.delete_isRkFinite_iff {α : Type u_1} {M : Matroid α} {D X : Set α} : (M.delete D).IsRkFinite X ↔ M.IsRkFinite (X \ D)

theorem Matroid.Coindep.delete_eRank_eq {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.Coindep X) : (M.delete X).eRank = M.eRank

theorem Matroid.eRank_delete_le {α : Type u_1} (M : Matroid α) (D : Set α) : (M.delete D).eRank ≤ M.eRank

theorem Matroid.Indep.delete_eRank_dual_eq {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) : (M.contract I)✶.eRank = M✶.eRank

theorem Matroid.Indep.eRank_dual_restrict_eq {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) : (M.restrict I)✶.eRank = 0

theorem Matroid.IsBasis.eRank_dual_restrict_of_disjoint {α : Type u_1} {M : Matroid α} {I X : Set α} (hB : M.IsBasis I (I ∪ X)) (hdj : Disjoint I X) : (M.restrict (I ∪ X))✶.eRank = X.encard

theorem Matroid.IsBasis.eRank_dual_restrict {α : Type u_1} {M : Matroid α} {I X : Set α} (hB : M.IsBasis I X) : (M.restrict X)✶.eRank = (X \ I).encard

@[simp]

theorem Matroid.eRank_dual_restrict_eq_zero_iff {α : Type u_1} {M : Matroid α} {I : Set α} : (M.restrict I)✶.eRank = 0 ↔ M.Indep I

theorem Matroid.Indep.contract_eRk_dual_eq {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) : (M.contract I)✶.eRank = M✶.eRank

theorem Matroid.eRank_project {α : Type u_1} (M : Matroid α) (C : Set α) : (M.project C).eRank = (M.contract C).eRank

theorem Matroid.eRk_project_eq_eRk_contract {α : Type u_1} (M : Matroid α) (C X : Set α) : (M.project C).eRk X = (M.contract C).eRk X

theorem Matroid.eRk_project_eq {α : Type u_1} (M : Matroid α) (C : Set α) : (M.project C).eRk = (M.contract C).eRk

noncomputable def Matroid.eRelRk {α : Type u_1} (M : Matroid α) (X Y : Set α) : ℕ∞

The relative ℕ∞-rank of sets X and Y, defined to be the ℕ∞-rank of Y in M ／ X, and equal to the minimum number of elements that need to be added to X to span Y. The definition suggests that X and Y should be disjoint, but it is also a natural expression when X ⊆ Y, and sometimes more generally.

Equations

• M.eRelRk X Y = (M.contract X).eRk Y

theorem Matroid.eRelRk_eq_eRk_contract {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eRelRk X Y = (M.contract X).eRk Y

theorem Matroid.eRelRk_eq_eRk_project {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eRelRk X Y = (M.project X).eRk Y

@[simp]

theorem Matroid.eRelRk_inter_ground_left {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eRelRk (X ∩ M.E) Y = M.eRelRk X Y

@[simp]

theorem Matroid.eRelRk_inter_ground_right {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eRelRk X (Y ∩ M.E) = M.eRelRk X Y

@[simp]

theorem Matroid.eRelRk_closure_left {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eRelRk (M.closure X) Y = M.eRelRk X Y

@[simp]

theorem Matroid.eRelRk_closure_right {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eRelRk X (M.closure Y) = M.eRelRk X Y

theorem Matroid.eRelRk_eq_eRk_diff_contract {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eRelRk X Y = (M.contract X).eRk (Y \ X)

@[simp]

theorem Matroid.eRelRk_empty_right {α : Type u_1} (M : Matroid α) (X : Set α) : M.eRelRk X ∅ = 0

@[simp]

theorem Matroid.eRelRk_empty_left {α : Type u_1} (M : Matroid α) (X : Set α) : M.eRelRk ∅ X = M.eRk X

theorem Matroid.eRelRk_eq_diff_right {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eRelRk X Y = M.eRelRk X (Y \ X)

theorem Matroid.eRelRk_eq_union_right {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eRelRk X Y = M.eRelRk X (Y ∪ X)

theorem Matroid.eRelRk_eq_zero_of_subset {α : Type u_1} {X Y : Set α} (M : Matroid α) (h : Y ⊆ X) : M.eRelRk X Y = 0

@[simp]

theorem Matroid.eRelRk_self {α : Type u_1} (M : Matroid α) (X : Set α) : M.eRelRk X X = 0

@[simp]

theorem Matroid.eRelRk_ground_left {α : Type u_1} (M : Matroid α) (X : Set α) : M.eRelRk M.E X = 0

theorem Matroid.eRelRk_eq_eRelRk_union {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eRelRk X Y = M.eRelRk X (Y ∪ X)

theorem Matroid.eRelRk_le_eRk {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eRelRk X Y ≤ M.eRk Y

theorem Matroid.eRelRk_mono_right {α : Type u_1} (M : Matroid α) (X : Set α) {Y Y' : Set α} (hYY' : Y ⊆ Y') : M.eRelRk X Y ≤ M.eRelRk X Y'

theorem Matroid.eRelRk_mono_left {α : Type u_1} (M : Matroid α) {X X' : Set α} (Y : Set α) (h : X ⊆ X') : M.eRelRk X' Y ≤ M.eRelRk X Y

theorem Matroid.IsBasis'.eRelRk_eq_encard_of_union_isBasis_disjoint {α : Type u_1} {M : Matroid α} {I J X Y : Set α} (hI : M.IsBasis' I X) (hIJ : M.IsBasis' (I ∪ J) Y) (hdj : Disjoint I J) : M.eRelRk X Y = J.encard

If Y contains a basis I for X, then M.eRelRk X Y is the number of elements that need to be added to I to give a basis for Y.

theorem Matroid.IsBasis'.eRelRk_eq_encard_diff {α : Type u_1} {M : Matroid α} {I C X : Set α} (hI : M.IsBasis' I (X ∪ C)) (hIC : M.IsBasis' (I ∩ C) C) : M.eRelRk C X = (I \ C).encard

If I is a basis for X ∪ C containing a basis for C, then the relative rank of C and X is the size of I \ C.

theorem Matroid.IsBasis.eRelRk_eq_encard_diff {α : Type u_1} {M : Matroid α} {I C X : Set α} (hI : M.IsBasis I (X ∪ C)) (hIC : M.IsBasis (I ∩ C) C) : M.eRelRk C X = (I \ C).encard

theorem Matroid.IsBasis'.eRelRk_eq_encard_diff_of_subset {α : Type u_1} {M : Matroid α} {I C X : Set α} (hI : M.IsBasis' I X) (hCX : C ⊆ X) (hIC : M.IsBasis' (I ∩ C) C) : M.eRelRk C X = (I \ C).encard

theorem Matroid.IsBasis.eRelRk_eq_encard_diff_of_subset {α : Type u_1} {M : Matroid α} {I C X : Set α} (hI : M.IsBasis I X) (hCX : C ⊆ X) (hIC : M.IsBasis (I ∩ C) C) : M.eRelRk C X = (I \ C).encard

theorem Matroid.Indep.eRelRk_of_subset {α : Type u_1} {M : Matroid α} {I J : Set α} (hI : M.Indep I) (hJ : J ⊆ I) : M.eRelRk J I = (I \ J).encard

theorem Matroid.IsBasis'.eRelRk_eq_encard_diff_of_subset_isBasis' {α : Type u_1} {M : Matroid α} {I J X Y : Set α} (hI : M.IsBasis' I X) (hJ : M.IsBasis' J Y) (hIJ : I ⊆ J) : M.eRelRk X Y = (J \ I).encard

theorem Matroid.IsBasis.eRelRk_eq_encard_diff_of_subset_isBasis {α : Type u_1} {M : Matroid α} {I J X Y : Set α} (hI : M.IsBasis I X) (hJ : M.IsBasis J Y) (hIJ : I ⊆ J) : M.eRelRk X Y = (J \ I).encard

theorem Matroid.eRelRk_le_eRk_diff {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eRelRk X Y ≤ M.eRk (Y \ X)

theorem Matroid.eRelRk_le_encard_diff {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eRelRk X Y ≤ (Y \ X).encard

theorem Matroid.eRelRk_insert_le {α : Type u_1} (M : Matroid α) (X : Set α) (e : α) : M.eRelRk X (insert e X) ≤ 1

theorem Matroid.eRelRk_add_eRk_of_subset {α : Type u_1} {X Y : Set α} (M : Matroid α) (hXY : X ⊆ Y) : M.eRelRk X Y + M.eRk X = M.eRk Y

theorem Matroid.eRelRk_add_eRk_eq {α : Type u_1} (M : Matroid α) (C X : Set α) : M.eRelRk C X + M.eRk C = M.eRk (X ∪ C)

theorem Matroid.eRelRk_union_add_eRk_inter_le {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eRelRk X (X ∪ Y) + M.eRk (X ∩ Y) ≤ M.eRk Y

theorem Matroid.IsRkFinite.eRelRk_eq_sub {α : Type u_1} {M : Matroid α} {X Y : Set α} (hY : M.IsRkFinite X) (hXY : X ⊆ Y) : M.eRelRk X Y = M.eRk Y - M.eRk X

theorem Matroid.IsNonloop.eRelRk_add_one_eq {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsNonloop e) (X : Set α) : M.eRelRk {e} X + 1 = M.eRk (insert e X)

theorem Matroid.IsNonloop.eRelRk_eq_sub_one {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsNonloop e) (X : Set α) : M.eRelRk {e} X = M.eRk (insert e X) - 1

theorem Matroid.eRelRk_add_cancel {α : Type u_1} {X Y Z : Set α} (M : Matroid α) (hXY : X ⊆ Y) (hYZ : Y ⊆ Z) : M.eRelRk X Y + M.eRelRk Y Z = M.eRelRk X Z

theorem Matroid.eRelRk_eq_zero_iff {α : Type u_1} {M : Matroid α} {X Y : Set α} (hY : Y ⊆ M.E := by aesop_mat) : M.eRelRk X Y = 0 ↔ Y ⊆ M.closure X

theorem Matroid.eRelRk_eq_zero_iff' {α : Type u_1} {M : Matroid α} {X Y : Set α} : M.eRelRk X Y = 0 ↔ Y ∩ M.E ⊆ M.closure X

theorem Matroid.IsBasis'.eRelRk_eq_zero {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.IsBasis' I X) : M.eRelRk I X = 0

theorem Matroid.IsBasis.eRelRk_eq_zero {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.IsBasis I X) : M.eRelRk I X = 0

theorem Matroid.eRelRk_insert_eq_zero_iff {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (he : e ∈ M.E := by aesop_mat) : M.eRelRk X (insert e X) = 0 ↔ e ∈ M.closure X

theorem Matroid.eRelRk_insert_eq_zero_iff' {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} : M.eRelRk X (insert e X) = 0 ↔ e ∈ M.E → e ∈ M.closure X

theorem Matroid.eRelRk_ground_eq_zero_iff {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X ⊆ M.E := by aesop_mat) : M.eRelRk X M.E = 0 ↔ M.Spanning X

theorem Matroid.eRelRk_eq_one_iff {α : Type u_1} {M : Matroid α} {X Y : Set α} (hY : Y ⊆ M.E := by aesop_mat) : M.eRelRk X Y = 1 ↔ ∃ e ∈ Y \ M.closure X, Y ⊆ M.closure (insert e X)

theorem Matroid.eRelRk_le_one_iff {α : Type u_1} {M : Matroid α} {X Y : Set α} (hYne : Y.Nonempty) (hY : Y ⊆ M.E := by aesop_mat) : M.eRelRk X Y ≤ 1 ↔ ∃ e ∈ Y, Y ⊆ M.closure (insert e X)

theorem Matroid.eRelRk_insert_eq_one {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (he : e ∈ M.E \ M.closure X) (hX : X ⊆ M.E := by aesop_mat) : M.eRelRk X (insert e X) = 1

theorem Matroid.eRelRk_diff_singleton_eq_one_iff {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (hX : X ⊆ M.E := by aesop_mat) : M.eRelRk (X \ {e}) X = 1 ↔ e ∈ X \ M.closure (X \ {e})

theorem Matroid.eRelRk_delete_eq_of_disjoint {α : Type u_1} {X Y : Set α} (M : Matroid α) {D : Set α} (hX : Disjoint X D) (hY : Disjoint Y D) : (M.delete D).eRelRk X Y = M.eRelRk X Y

theorem Matroid.eRelRk_delete_eq {α : Type u_1} (M : Matroid α) (X Y D : Set α) : (M.delete D).eRelRk X Y = M.eRelRk (X \ D) (Y \ D)

theorem Matroid.eRelRk_ground_le_iff {α : Type u_1} {M : Matroid α} {X : Set α} {k : ℕ} (hX : X ⊆ M.E) : M.eRelRk X M.E ≤ ↑k ↔ ∃ (D : Finset α), ↑D ⊆ M.E ∧ D.card ≤ k ∧ M.Spanning (X ∪ ↑D)

theorem Matroid.eRelRk_union_le_eRelRk_inter_right {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eRelRk X (X ∪ Y) ≤ M.eRelRk (X ∩ Y) Y

theorem Matroid.eRelRk_union_le_eRelRk_inter_left {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eRelRk Y (X ∪ Y) ≤ M.eRelRk (X ∩ Y) X

theorem Matroid.eRelRk_union_add_eRelRk_union_le_eRelRk_inter_union {α : Type u_1} {M : Matroid α} (X Y : Set α) : M.eRelRk X (X ∪ Y) + M.eRelRk Y (X ∪ Y) ≤ M.eRelRk (X ∩ Y) (X ∪ Y)

theorem Matroid.eRelRk_restrict_eq_of_subset {α : Type u_1} {X Y : Set α} (M : Matroid α) {R : Set α} (hX : X ⊆ R) (hY : Y ⊆ R) : (M.restrict R).eRelRk X Y = M.eRelRk X Y

@[simp]

theorem Matroid.eRelRk_restrict {α : Type u_1} (M : Matroid α) (R X Y : Set α) : (M.restrict R).eRelRk X Y = M.eRelRk (X ∩ R) (Y ∩ R)

theorem Matroid.eRelRk_project_eq_eRelRk_contract {α : Type u_1} (M : Matroid α) (C X Y : Set α) : (M.project C).eRelRk X Y = (M.contract C).eRelRk X Y

theorem Matroid.RankPos.of_delete {α : Type u_1} {M : Matroid α} {D : Set α} (h : (M.delete D).RankPos) : M.RankPos

theorem Matroid.eRk_contract_le_eRk_delete {α : Type u_1} (M : Matroid α) (X Y : Set α) : (M.contract X).eRk Y ≤ (M.delete X).eRk Y

theorem Matroid.eRk_contract_le_eRk {α : Type u_1} (M : Matroid α) (C X : Set α) : (M.contract C).eRk X ≤ M.eRk X

theorem Matroid.eRank_contract_le_eRank_delete {α : Type u_1} (M : Matroid α) (X : Set α) : (M.contract X).eRank ≤ (M.delete X).eRank

theorem Matroid.eRank_contract_le {α : Type u_1} (M : Matroid α) (C : Set α) : (M.contract C).eRank ≤ M.eRank

theorem Matroid.eRank_contract_add_eRk {α : Type u_1} (M : Matroid α) (C : Set α) : (M.contract C).eRank + M.eRk C = M.eRank

theorem Matroid.eRk_contract_add_eRk {α : Type u_1} (M : Matroid α) (X C : Set α) : (M.contract C).eRk X + M.eRk C = M.eRk (X ∪ C)

theorem Matroid.IsNonloop.eRank_contractElem_add_one {α : Type u_1} {e : α} (M : Matroid α) (he : M.IsNonloop e) : (M.contract {e}).eRank + 1 = M.eRank

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

theorem Matroid.IsRkFinite.union_of_contract {α : Type u_1} {M : Matroid α} {C X : Set α} (hX : (M.contract C).IsRkFinite X) (hC : M.IsRkFinite C) : M.IsRkFinite (X ∪ C)

theorem Matroid.IsRkFinite.of_contract {α : Type u_1} {M : Matroid α} {C X : Set α} (hX : (M.contract C).IsRkFinite X) (hC : M.IsRkFinite C) : M.IsRkFinite X

theorem Matroid.IsRkFinite.contract_isRkFinite_of_subset_union {α : Type u_1} {M : Matroid α} {Z : Set α} (h : M.IsRkFinite Z) (X C : Set α) (hX : X ⊆ M.closure (Z ∪ C)) : (M.contract C).IsRkFinite (X \ C)

theorem Matroid.IsMinor.eRank_le {α : Type u_1} {M N : Matroid α} (h : N ≤m M) : N.eRank ≤ M.eRank

theorem Matroid.IsMinor.rank_le {α : Type u_1} {M N : Matroid α} (h : N ≤m M) [M.RankFinite] : N.rank ≤ M.rank

theorem Matroid.eRk_delete_le_eRk {α : Type u_1} {D : Set α} (M : Matroid α) (X : Set α) : (M.delete D).eRk X ≤ M.eRk X

theorem Matroid.IsMinor.eRk_le {α : Type u_1} {M N : Matroid α} (h : N ≤m M) (X : Set α) : N.eRk X ≤ M.eRk X

theorem Matroid.eRelRk_contract_le {α : Type u_1} (M : Matroid α) (C X Y : Set α) : (M.contract C).eRelRk X Y ≤ M.eRelRk X Y

theorem Matroid.eRank_contract_eq_eRelRk_ground {α : Type u_1} (M : Matroid α) (C : Set α) : (M.contract C).eRank = M.eRelRk C M.E

theorem Matroid.eRank_contract_eq_zero_iff {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X ⊆ M.E := by aesop_mat) : (M.contract X).eRank = 0 ↔ M.Spanning X

theorem Matroid.Spanning.eRank_contract {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.Spanning X) : (M.contract X).eRank = 0

theorem Matroid.contractElem_eRank_add_one_ge_eRank {α : Type u_1} (M : Matroid α) (e : α) : M.eRank ≤ (M.contract {e}).eRank + 1

theorem Matroid.deleteElem_eRank_eq {α : Type u_1} {M : Matroid α} {e : α} (he : ¬M.IsColoop e) : (M.delete {e}).eRank = M.eRank

theorem Matroid.delete_elem_rank_eq {α : Type u_1} {e : α} (M : Matroid α) (he : ¬M.IsColoop e) : (M.delete {e}).rank = M.rank

theorem Matroid.delete_rk_eq' {α : Type u_1} (M : Matroid α) (D X : Set α) : (M.delete D).rk X = M.rk (X \ D)

theorem Matroid.delete_rk_eq_of_disjoint {α : Type u_1} {D X : Set α} (M : Matroid α) (hDX : Disjoint X D) : (M.delete D).rk X = M.rk X

theorem Matroid.deleteElem_rk_eq {α : Type u_1} {X : Set α} {e : α} (M : Matroid α) (heX : e ∉ X) : (M.delete {e}).rk X = M.rk X

theorem Matroid.restrict_rk_eq' {α : Type u_1} (M : Matroid α) (R X : Set α) : (M.restrict R).rk X = M.rk (X ∩ R)

theorem Matroid.restrict_rk_eq {α : Type u_1} {X : Set α} (M : Matroid α) {R : Set α} (hXR : X ⊆ R) : (M.restrict R).rk X = M.rk X

theorem Matroid.delete_rank_le {α : Type u_1} (M : Matroid α) [M.RankFinite] (D : Set α) : (M.delete D).rank ≤ M.rank

theorem Matroid.delete_eRank_add_eRk_ge_eRank {α : Type u_1} (M : Matroid α) (D : Set α) : M.eRank ≤ (M.delete D).eRank + M.eRk D

theorem Matroid.deleteElem_eRank_add_one_ge_eRank {α : Type u_1} (M : Matroid α) (e : α) : M.eRank ≤ (M.delete {e}).eRank + 1

theorem Matroid.removeElem_eRank_add_one_ge_eRank {α : Type u_1} (M : Matroid α) (e : α) (b : Bool) : M.eRank ≤ (M.remove b {e}).eRank + 1

theorem Matroid.delete_rank_add_rk_ge_rank {α : Type u_1} (M : Matroid α) (D : Set α) : M.rank ≤ (M.delete D).rank + M.rk D

theorem Matroid.contract_rk_add_eq {α : Type u_1} (M : Matroid α) [M.RankFinite] (C X : Set α) : (M.contract C).rk X + M.rk C = M.rk (X ∪ C)

@[simp]

theorem Matroid.contract_rk_cast_int_eq {α : Type u_1} (M : Matroid α) [M.RankFinite] (C X : Set α) : ↑((M.contract C).rk X) = ↑(M.rk (X ∪ C)) - ↑(M.rk C)

@[simp]

theorem Matroid.contract_rank_cast_int_eq {α : Type u_1} (M : Matroid α) [M.RankFinite] (C : Set α) : ↑(M.contract C).rank = ↑M.rank - ↑(M.rk C)

theorem Matroid.IsNonloop.contractElem_rk_add_one_eq {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} [M.RankFinite] (he : M.IsNonloop e) : (M.contract {e}).rk X + 1 = M.rk (insert e X)

theorem Matroid.IsNonloop.contractElem_rank_add_one_eq {α : Type u_1} {M : Matroid α} {e : α} [M.RankFinite] (he : M.IsNonloop e) : (M.contract {e}).rank + 1 = M.rank

theorem Matroid.IsNonloop.contractElem_rk_intCast_eq {α : Type u_1} {X : Set α} {e : α} (M : Matroid α) [M.RankFinite] (he : M.IsNonloop e) : ↑((M.contract {e}).rk X) = ↑(M.rk (insert e X)) - 1

theorem Matroid.RankFinite.ofDelete {α : Type u_1} {M : Matroid α} {D : Set α} (hD : M.IsRkFinite D) (hfin : (M.delete D).RankFinite) : M.RankFinite

Move to minor

theorem Matroid.Indep.nullity_contract_of_superset {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.Indep I) (hIX : I ⊆ X) : (M.contract I).nullity (X \ I) = M.nullity X

theorem Matroid.nullity_eq_eRelRk {α : Type u_1} (M : Matroid α) (X : Set α) (hXE : X ⊆ M.E := by aesop_mat) : M.nullity X = M✶.eRelRk (M.E \ X) M.E

theorem Matroid.nullity_dual_eq {α : Type u_1} (M : Matroid α) (X : Set α) (hXE : X ⊆ M.E := by aesop_mat) : M✶.nullity X = M.eRelRk (M.E \ X) M.E

theorem Matroid.nullity_compl_dual_eq {α : Type u_1} (M : Matroid α) (X : Set α) : M✶.nullity (M.E \ X) = M.eRelRk X M.E

theorem Matroid.nullity_delete {α : Type u_1} {D X : Set α} (M : Matroid α) (hXD : Disjoint X D) : (M.delete D).nullity X = M.nullity X

theorem Matroid.nullity_delete_le {α : Type u_1} (M : Matroid α) (X D : Set α) : (M.delete D).nullity (X \ D) ≤ M.nullity X

theorem Matroid.nullity_contract_le {α : Type u_1} {C X : Set α} (M : Matroid α) (hCX : C ⊆ X) : (M.contract C).nullity (X \ C) ≤ M.nullity X

theorem Matroid.nullity_contract_ge_of_disjoint {α : Type u_1} {C X : Set α} (M : Matroid α) (hXC : Disjoint X C) : M.nullity X ≤ (M.contract C).nullity X

noncomputable def Matroid.relRk {α : Type u_1} {M : Matroid α} (X Y : Set α) : ℕ

M.relRk X Y is the relative rank of X and Y as a natural number. If M.eRelRk X Y is infinite, this has the junk value of zero. If Y has finite rank and X ⊆ Y, then this is the difference between the ranks of X and Y.

Equations

• Matroid.relRk X Y = (M.eRelRk X Y).toNat

theorem Matroid.relRk_intCast_eq_sub {α : Type u_1} (M : Matroid α) [M.RankFinite] (X Y : Set α) : ↑(relRk X Y) = ↑(M.rk (X ∪ Y)) - ↑(M.rk X)

theorem Matroid.relRk_intCast_eq_sub_of_subset {α : Type u_1} {X Y : Set α} (M : Matroid α) [M.RankFinite] (hXY : X ⊆ Y) : ↑(relRk X Y) = ↑(M.rk Y) - ↑(M.rk X)

theorem Matroid.exists_contract_eRank_eq {α : Type u_1} {a : ℕ∞} (M : Matroid α) (hr : a ≤ M.eRank) : ∃ X ⊆ M.E, (M.contract X).eRank = a

theorem Matroid.exists_contract_eRk_eq {α : Type u_1} {a : ℕ∞} (M : Matroid α) (X : Set α) (hr : a ≤ M.eRk X) : ∃ C ⊆ X, (M.contract C).eRk (X \ C) = a

@[simp]

theorem Matroid.delete_rkLE_iff {α : Type u_1} {M : Matroid α} {D X : Set α} {k : ℕ∞} : (M.delete D).RkLE k X ↔ M.RkLE k (X \ D)

@[simp]

theorem Matroid.restrict_rkLE_iff {α : Type u_1} {M : Matroid α} {X : Set α} {k : ℕ∞} {R : Set α} : (M.restrict R).RkLE k X ↔ M.RkLE k (X ∩ R)

theorem Matroid.IsRkFinite.contract_rkLE_iff {α : Type u_1} {M : Matroid α} {C X : Set α} {k : ℕ∞} (h : M.IsRkFinite C) : (M.contract C).RkLE k X ↔ M.RkLE (k + M.eRk C) (X ∪ C)

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

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

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

theorem Matroid.RkLE.minor {α : Type u_1} {M N : Matroid α} {X : Set α} {k : ℕ∞} (h : M.RkLE k X) (hNM : N ≤m M) : N.RkLE k X

theorem Matroid.RkLE.union_of_contract {α : Type u_1} {M : Matroid α} {C X : Set α} {k : ℕ∞} (h : (M.contract C).RkLE k X) : M.RkLE (k + M.eRk C) (X ∪ C)

theorem Matroid.RkLE.of_contract {α : Type u_1} {M : Matroid α} {C X : Set α} {k : ℕ∞} (h : (M.contract C).RkLE k X) : M.RkLE (k + M.eRk C) X