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

The rank-deficiency of a set, as a term in ℕ∞. Cannot be defined with subtraction. For the ℕ version, the simpler expression X.ncard - M.r X is preferable.

To reduce the number of X ⊆ M.E assumptions needed for lemmas, this is defined so that junk elements in X \ M.E contribute to the nullity of X in M, so M.nullity X = M.nullity (X ∩ M.E) + (X \ M.E).encard. (see Matroid.nullity_eq_nullity_inter_ground_add_encard_diff )

Equations

• M.nullity X = (M.restrict X)✶.eRank

theorem Matroid.nullity_eq_eRank_restrict_dual {α : Type u_1} (M : Matroid α) (X : Set α) : M.nullity X = (M.restrict X)✶.eRank

theorem Matroid.nullity_eq_eRank_dual_contract {α : Type u_1} (M : Matroid α) (X : Set α) (hX : X ⊆ M.E := by aesop_mat) : M.nullity X = (M✶.contract (M.E \ X)).eRank

theorem Matroid.nullity_restrict_of_subset {α : Type u_1} {X Y : Set α} (M : Matroid α) (hXY : X ⊆ Y) : (M.restrict Y).nullity X = M.nullity X

theorem Matroid.nullity_restrict_self {α : Type u_1} (M : Matroid α) (X : Set α) : (M.restrict X).nullity X = M.nullity X

@[simp]

theorem Matroid.nullity_restrict_univ {α : Type u_1} (M : Matroid α) : (M.restrict Set.univ).nullity = M.nullity

theorem Matroid.IsBasis'.nullity_eq {α : Type u_1} {M : Matroid α} {I X : Set α} (hIX : M.IsBasis' I X) : M.nullity X = (X \ I).encard

theorem Matroid.IsBasis.nullity_eq {α : Type u_1} {M : Matroid α} {I X : Set α} (hIX : M.IsBasis I X) : M.nullity X = (X \ I).encard

@[simp]

theorem Matroid.eRk_add_nullity_eq_encard {α : Type u_1} (M : Matroid α) (X : Set α) : M.eRk X + M.nullity X = X.encard

@[simp]

theorem Matroid.nullity_add_eRk_add_eq_encard {α : Type u_1} (M : Matroid α) (X : Set α) : M.nullity X + M.eRk X = X.encard

theorem Matroid.nullity_le_encard {α : Type u_1} (M : Matroid α) (X : Set α) : M.nullity X ≤ X.encard

theorem Matroid.Indep.nullity_eq {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) : M.nullity I = 0

@[simp]

theorem Matroid.nullity_empty {α : Type u_1} (M : Matroid α) : M.nullity ∅ = 0

@[simp]

theorem Matroid.nullity_eq_zero {α : Type u_1} {M : Matroid α} {I : Set α} : M.nullity I = 0 ↔ M.Indep I

theorem Matroid.Dep.one_le_nullity {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.Dep X) : 1 ≤ M.nullity X

theorem Matroid.one_le_nullity_iff {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X ⊆ M.E := by aesop_mat) : 1 ≤ M.nullity X ↔ M.Dep X

theorem Matroid.nullity_eq_encard {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X ⊆ M.loops) : M.nullity X = X.encard

theorem Matroid.IsCircuit.nullity_eq {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) : M.nullity C = 1

theorem Matroid.IsNonloop.nullity_eq {α : Type u_1} {M : Matroid α} {e : α} (h : M.IsNonloop e) : M.nullity {e} = 0

theorem Matroid.IsLoop.nullity_eq {α : Type u_1} {M : Matroid α} {e : α} (h : M.IsLoop e) : M.nullity {e} = 1

@[simp]

theorem Matroid.nullity_singleton_eq_one {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) : M.nullity {e} = 1 ↔ M.IsLoop e

theorem Matroid.nullity_singleton_eq_ite {α : Type u_1} {M : Matroid α} {e : α} [Decidable (M.IsLoop e)] (he : e ∈ M.E := by aesop_mat) : M.nullity {e} = if M.IsLoop e then 1 else 0

theorem Matroid.nullity_singleton_eq_ite' {α : Type u_1} {M : Matroid α} {e : α} [Decidable (M.IsNonloop e)] : M.nullity {e} = if M.IsNonloop e then 0 else 1

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

theorem Matroid.nullity_insert_eq_add_one {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (hecl : e ∈ M.closure X) (heX : e ∉ X) : M.nullity (insert e X) = M.nullity X + 1

theorem Matroid.nullity_eq_nullity_inter_ground_add_encard_diff {α : Type u_1} (M : Matroid α) (X : Set α) : M.nullity X = M.nullity (X ∩ M.E) + (X \ M.E).encard

theorem Matroid.Indep.nullity_le_encard_diff_of_subset {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.Indep I) (hIX : I ⊆ X) : M.nullity X ≤ (X \ I).encard

theorem Matroid.nullity_corestrict_univ_eq {α : Type u_1} (M : Matroid α) (X : Set α) (hX : X ⊆ M.E := by aesop_mat) : (M✶.restrict Set.univ)✶.nullity X = M.nullity X

theorem Matroid.nullity_corestrict_univ_eq_nullity_inter {α : Type u_1} (M : Matroid α) (X : Set α) : (M✶.restrict Set.univ)✶.nullity X = M.nullity (X ∩ M.E)

theorem Matroid.nullity_insert {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (heX : e ∉ M.closure X) (heE : e ∈ M.E := by aesop_mat) : M.nullity (insert e X) = M.nullity X

theorem Matroid.nullity_union_eq_nullity_contract_add_nullity {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.nullity (X ∪ Y) = (M.contract X).nullity (Y \ X) + M.nullity X

theorem Matroid.nullity_union_eq_nullity_add_encard_diff {α : Type u_1} {M : Matroid α} {X Y : Set α} (hYX : Y ⊆ M.closure X) : M.nullity (X ∪ Y) = M.nullity X + (Y \ X).encard

theorem Matroid.nullity_union_le_nullity_add_encard_diff {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.nullity (X ∪ Y) ≤ M.nullity X + (Y \ X).encard

theorem Matroid.nullity_union_le_nullity_add_encard {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.nullity (X ∪ Y) ≤ M.nullity X + Y.encard

theorem Matroid.nullity_eq_nullity_add_encard_diff {α : Type u_1} {M : Matroid α} {X Y : Set α} (hXY : X ⊆ Y) (hYX : Y ⊆ M.closure X) : M.nullity Y = M.nullity X + (Y \ X).encard

theorem Matroid.nullity_eq_nullity_diff_loops_add_encard {α : Type u_1} (M : Matroid α) (X : Set α) : M.nullity X = M.nullity (X \ M.loops) + (X ∩ M.loops).encard

theorem Matroid.Disjoint.nullity_union_eq_of_subset_closure {α : Type u_1} {M : Matroid α} {X Y : Set α} (hXY : Disjoint X Y) (hYX : Y ⊆ M.closure X) : M.nullity (X ∪ Y) = M.nullity X + Y.encard

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

theorem Matroid.nullity_add_nullity_le_nullity_union {α : Type u_1} {X Y : Set α} (M : Matroid α) (hdj : Disjoint X Y) : M.nullity X + M.nullity Y ≤ M.nullity (X ∪ Y)

theorem Matroid.nullity_delete_of_disjoint {α : Type u_1} {X Y : Set α} (M : Matroid α) (hXY : Disjoint X Y) : (M.delete Y).nullity X = M.nullity X

theorem Matroid.nullity_project_ge {α : Type u_1} (M : Matroid α) (C X : Set α) : M.nullity X ≤ (M.project C).nullity X

theorem Matroid.nullity_project_mono {α : Type u_1} {C C' : Set α} (M : Matroid α) (hCC' : C ⊆ C') (X : Set α) : (M.project C).nullity X ≤ (M.project C').nullity X

theorem Matroid.nullity_project_add_nullity_eq {α : Type u_1} (M : Matroid α) (C X : Set α) : (M.project C).nullity X + M.nullity C = M.nullity (X ∪ C) + (X ∩ C).encard

theorem Matroid.nullity_project_of_disjoint {α : Type u_1} {X : Set α} (M : Matroid α) {C : Set α} (hCX : Disjoint X C) : (M.project C).nullity X + M.nullity C = M.nullity (X ∪ C)

theorem Matroid.Indep.nullity_project {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) (X : Set α) : (M.project I).nullity X = M.nullity (X ∪ I) + (X ∩ I).encard

theorem Matroid.Indep.nullity_project_of_disjoint {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.Indep I) (hdj : Disjoint I X) : (M.project I).nullity X = M.nullity (I ∪ X)

theorem Matroid.nullity_project_add_nullity_comm {α : Type u_1} (M : Matroid α) (X Y : Set α) : (M.project X).nullity Y + M.nullity X = (M.project Y).nullity X + M.nullity Y

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

theorem Matroid.nullity_union_eq_nullity_project_add_nullity {α : Type u_1} {X Y : Set α} (M : Matroid α) (hXY : Disjoint X Y) : M.nullity (X ∪ Y) = (M.project X).nullity Y + M.nullity X

theorem Matroid.nullity_project_le_of_le {α : Type u_1} {M : Matroid α} {X Y C : Set α} (hn : M.nullity X ≤ M.nullity Y) (hcl : M.closure X ⊆ M.closure Y) : (M.project C).nullity X ≤ (M.project C).nullity Y

theorem Matroid.nullity_project_congr {α : Type u_1} {M : Matroid α} {X Y C : Set α} (hn : M.nullity X = M.nullity Y) (hcl : M.closure X = M.closure Y) : (M.project C).nullity X = (M.project C).nullity Y

theorem Matroid.IsBasis'.nullity_project {α : Type u_1} {M : Matroid α} {I X C J : Set α} (hI : M.IsBasis' I X) (hJ : M.IsBasis' J X) : (M.project C).nullity I = (M.project C).nullity J

theorem Matroid.IsBasis.nullity_project {α : Type u_1} {M : Matroid α} {I X C J : Set α} (hI : M.IsBasis I X) (hJ : M.IsBasis J X) : (M.project C).nullity I = (M.project C).nullity J

theorem Matroid.nullity_comap {α : Type u_3} {β : Type u_4} {f : α → β} (M : Matroid β) (X : Set α) (hX : Set.InjOn f X) : (M.comap f).nullity X = M.nullity (f '' X)

theorem Matroid.nullity_map_image {α : Type u_1} {M : Matroid α} {β : Type u_3} {f : α → β} (hf : Set.InjOn f M.E) {X : Set α} (hX : X ⊆ M.E) : (M.map f hf).nullity (f '' X) = M.nullity X

theorem Matroid.Indep.exists_subset_supset_nullity_eq {α : Type u_1} {M : Matroid α} {I X : Set α} {k : ℕ∞} (hI : M.Indep I) (hIX : I ⊆ X) (hk : k ≤ M.nullity X) : ∃ Y ⊆ X, I ⊆ Y ∧ M.nullity Y = k

theorem Matroid.exists_subset_nullity_eq {α : Type u_1} {M : Matroid α} {X : Set α} {k : ℕ∞} (hk : k ≤ M.nullity X) : ∃ Y ⊆ X, M.nullity Y = k

theorem Matroid.IsCircuit.two_le_nullity_union_of_ne {α : Type u_1} {M : Matroid α} {C C' : Set α} (hC : M.IsCircuit C) (hC' : M.IsCircuit C') (hCC' : C ≠ C') : 2 ≤ M.nullity (C ∪ C')

theorem Matroid.Cyclic.two_le_nullity_union_of_ne {α : Type u_1} {M : Matroid α} {C C' : Set α} (hC : M.Cyclic C) (hCne : C.Nonempty) (hC' : M.Cyclic C') (hC'ne : C'.Nonempty) (hCC' : C ≠ C') : 2 ≤ M.nullity (C ∪ C')