@[reducible, inline]

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

the connectivity function of a matroid as a pure function, rather than a ConnSystem. Just an implementation detail on the way to a ConnSystem; not intended for external use.

Equations

• M.eConnAux X = M.eLocalConn X (M.E \ X)

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

noncomputable def Matroid.eConn {α : Type u_1} (M : Matroid α) : ConnSystem α ℕ∞

The connectivity function of a matroid, given as a ConnSystem.

Equations

• M.eConn = { E := M.E, toFun := M.eConnAux, toFun_inter_ground := ⋯, toFun_compl := ⋯, toFun_submod := ⋯ }

theorem Matroid.eConn_eq_eLocalConn {α : Type u_1} (M : Matroid α) (X : Set α) : ↑M.eConn X = M.eLocalConn X (M.E \ X)

@[simp]

theorem Matroid.eConn_ground_eq {α : Type u_1} (M : Matroid α) : M.eConn.E = M.E

@[simp]

theorem Matroid.eConn_inter_ground {α : Type u_1} (M : Matroid α) (X : Set α) : ↑M.eConn (X ∩ M.E) = ↑M.eConn X

theorem Matroid.eConn_unitary {α : Type u_1} (M : Matroid α) : M.eConn.Unitary

@[simp]

theorem Matroid.eConn_empty {α : Type u_1} (M : Matroid α) : ↑M.eConn ∅ = 0

@[simp]

theorem Matroid.loopyOn_eConn {α : Type u_1} (E X : Set α) : ↑(loopyOn E).eConn X = 0

@[simp]

theorem Matroid.eConn_ground {α : Type u_1} (M : Matroid α) : ↑M.eConn M.E = 0

instance Matroid.instInvariantFunSetENatToFunEConn : InvariantFun (fun {α : Type u_3} (M : Matroid α) => ↑M.eConn) fun {α : Type u_4} (M : Matroid α) => ↑M.eConn

theorem Matroid.map_eConn_image {α : Type u_1} {M : Matroid α} {X : Set α} {β : Type u_3} {f : α → β} (hf : Set.InjOn f M.E) (hXE : X ⊆ M.E) : ↑(M.map f hf).eConn (f '' X) = ↑M.eConn X

theorem Matroid.map_eConn {α : Type u_1} {M : Matroid α} {β : Type u_3} {f : α → β} (hf : Set.InjOn f M.E) (X : Set β) : ↑(M.map f hf).eConn X = ↑M.eConn (f ⁻¹' X ∩ M.E)

@[simp]

theorem Matroid.eConn_dual {α : Type u_1} (M : Matroid α) : M✶.eConn = M.eConn

Connectivity is self-dual.

@[simp]

theorem Matroid.eConn_bDual {α : Type u_1} (M : Matroid α) (b : Bool) : (M.bDual b).eConn = M.eConn

theorem Matroid.IsBasis'.eConn_eq {α : Type u_1} {M : Matroid α} {I J X : Set α} (hIX : M.IsBasis' I X) (hJX : M.IsBasis' J (M.E \ X)) : ↑M.eConn X = M.nullity (I ∪ J)

theorem Matroid.IsBasis.eConn_eq {α : Type u_1} {M : Matroid α} {I J X : Set α} (hIX : M.IsBasis I X) (hJX : M.IsBasis J (M.E \ X)) : ↑M.eConn X = M.nullity (I ∪ J)

theorem Matroid.IsBasis.eConn_eq' {α : Type u_1} {M : Matroid α} {I J X : Set α} (hIX : M.IsBasis I X) (hJX : M.IsBasis J Xᶜ) : ↑M.eConn X = M.nullity (I ∪ J)

theorem Matroid.eConn_eq_eLocalConn' {α : Type u_1} (M : Matroid α) (X : Set α) : ↑M.eConn X = M.eLocalConn (X ∩ M.E) (M.E \ X)

@[simp]

theorem Matroid.removeLoops_eConn {α : Type u_1} (M : Matroid α) (X : Set α) : ↑M.removeLoops.eConn X = ↑M.eConn X

theorem Matroid.eConn_union_of_subset_loops {α : Type u_1} {M : Matroid α} {X L : Set α} (hL : L ⊆ M.loops) : ↑M.eConn (X ∪ L) = ↑M.eConn X

theorem Matroid.eConn_diff_of_subset_loops {α : Type u_1} {M : Matroid α} {X L : Set α} (hL : L ⊆ M.loops) : ↑M.eConn (X \ L) = ↑M.eConn X

theorem Matroid.Indep.nullity_union_le_eConn {α : Type u_1} {M : Matroid α} {I J X : Set α} (hI : M.Indep I) (hJ : M.Indep J) (hIX : I ⊆ X) (hJX : Disjoint J X) : M.nullity (I ∪ J) ≤ ↑M.eConn X

@[simp]

theorem Matroid.eConn_restrict_univ_eq {α : Type u_1} (M : Matroid α) (X : Set α) : ↑(M.restrict Set.univ).eConn X = ↑M.eConn X

@[simp]

theorem Matroid.eConn_corestrict_univ_eq {α : Type u_1} (M : Matroid α) (X : Set α) : ↑(M✶.restrict Set.univ)✶.eConn X = ↑M.eConn X

@[simp]

theorem Matroid.eConn_compl {α : Type u_1} (M : Matroid α) (X : Set α) : ↑M.eConn (M.E \ X) = ↑M.eConn X

@[simp]

theorem Matroid.eConn_compl' {α : Type u_1} (M : Matroid α) (X : Set α) : ↑M.eConn Xᶜ = ↑M.eConn X

A version of eConn_compl where compl really means complementation in the universe.

theorem Matroid.IsBasis'.eConn_eq_nullity_contract {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.IsBasis' I X) : ↑M.eConn X = (M.contract (M.E \ X)).nullity I

theorem Matroid.IsBasis.eConn_eq_nullity_contract {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.IsBasis I X) : ↑M.eConn X = (M.contract (M.E \ X)).nullity I

theorem Matroid.eConn_union_of_subset_coloops {α : Type u_1} {M : Matroid α} {X L : Set α} (hL : L ⊆ M.coloops) : ↑M.eConn (X ∪ L) = ↑M.eConn X

theorem Matroid.eConn_diff_of_subset_coloops {α : Type u_1} {M : Matroid α} {X L : Set α} (hL : L ⊆ M.coloops) : ↑M.eConn (X \ L) = ↑M.eConn X

theorem Matroid.eConn_delete_eq_of_subset_loops {α : Type u_1} {M : Matroid α} {X L : Set α} (hL : L ⊆ M.loops) : ↑(M.delete L).eConn X = ↑M.eConn X

theorem Matroid.eConn_delete_eq_diff_of_subset_loops {α : Type u_1} {M : Matroid α} {X L : Set α} (hL : L ⊆ M.loops) : ↑(M.delete L).eConn X = ↑M.eConn (X \ L)

theorem Matroid.eConn_contract_of_subset_coloops {α : Type u_1} {M : Matroid α} {X L : Set α} (hL : L ⊆ M.coloops) : ↑(M.contract L).eConn X = ↑M.eConn X

theorem Matroid.eConn_contract_eq_diff_of_subset_coloops {α : Type u_1} {M : Matroid α} {X L : Set α} (hL : L ⊆ M.coloops) : ↑(M.contract L).eConn X = ↑M.eConn (X \ L)

@[simp]

theorem Matroid.eConn_loops {α : Type u_1} (M : Matroid α) : ↑M.eConn M.loops = 0

@[simp]

theorem Matroid.eConn_coloops {α : Type u_1} (M : Matroid α) : ↑M.eConn M.coloops = 0

@[simp]

theorem Matroid.eConn_union_loops {α : Type u_1} (M : Matroid α) (X : Set α) : ↑M.eConn (X ∪ M.loops) = ↑M.eConn X

@[simp]

theorem Matroid.eConn_union_coloops {α : Type u_1} (M : Matroid α) (X : Set α) : ↑M.eConn (X ∪ M.coloops) = ↑M.eConn X

theorem Matroid.eConn_subset_loops {α : Type u_1} {M : Matroid α} {X : Set α} (h : X ⊆ M.loops) : ↑M.eConn X = 0

theorem Matroid.eConn_subset_coloops {α : Type u_1} {M : Matroid α} {X : Set α} (h : X ⊆ M.coloops) : ↑M.eConn X = 0

theorem Matroid.eConn_of_subset_loops_union_coloops {α : Type u_1} {M : Matroid α} {X : Set α} (h : X ⊆ M.loops ∪ M.coloops) : ↑M.eConn X = 0

@[simp]

theorem Matroid.uniqueBaseon_eConn {α : Type u_1} (E B X : Set α) : ↑(uniqueBaseOn B E).eConn X = 0

theorem Matroid.eRk_add_eRk_compl_eq {α : Type u_1} (M : Matroid α) (X : Set α) : M.eRk X + M.eRk (M.E \ X) = M.eRank + ↑M.eConn X

theorem Matroid.eConn_le_eRk {α : Type u_1} (M : Matroid α) (X : Set α) : ↑M.eConn X ≤ M.eRk X

theorem Matroid.eConn_le_eRk_dual {α : Type u_1} (M : Matroid α) (X : Set α) : ↑M.eConn X ≤ M✶.eRk X

theorem Matroid.eConn_le_encard {α : Type u_1} (M : Matroid α) (X : Set α) : ↑M.eConn X ≤ X.encard

@[simp]

theorem Matroid.freeOn_eConn {α : Type u_1} (E X : Set α) : ↑(freeOn E).eConn X = 0

theorem Matroid.eConn_add_nullity_dual_eq_eRk {α : Type u_1} (M : Matroid α) (X : Set α) (hX : X ⊆ M.E := by aesop_mat) : ↑M.eConn X + M✶.nullity X = M.eRk X

The slack term in the inequality λ(X) ≤ r(X) is co-nullity

theorem Matroid.eConn_add_nullity_dual_eq_eRk' {α : Type u_1} (M : Matroid α) (X : Set α) : ↑M.eConn X + M✶.nullity X = M.eRk X + (X \ M.E).encard

theorem Matroid.eConn_add_nullity_eq_eRk_dual {α : Type u_1} (M : Matroid α) (X : Set α) (hX : X ⊆ M.E := by aesop_mat) : ↑M.eConn X + M.nullity X = M✶.eRk X

The slack term in the inequality λ(X) ≤ r✶(X) is nullity

theorem Matroid.Indep.eConn_eq_eRk_dual {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) : ↑M.eConn I = M✶.eRk I

theorem Matroid.eConn_add_eRank_eq {α : Type u_1} {X : Set α} (M : Matroid α) : ↑M.eConn X + M.eRank = M.eRk X + M.eRk (M.E \ X)

theorem Matroid.Indep.eConn_eq_of_compl_indep {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) (hI' : M.Indep (M.E \ I)) : ↑M.eConn I = M✶.eRank

theorem Matroid.eConn_union_eq_of_subset_loops {α : Type u_1} {M : Matroid α} {Y : Set α} (X : Set α) (hY : Y ⊆ M.loops) : ↑M.eConn (X ∪ Y) = ↑M.eConn X

theorem Matroid.eConn_union_eq_of_subset_coloops {α : Type u_1} {M : Matroid α} {Y : Set α} (X : Set α) (hY : Y ⊆ M.coloops) : ↑M.eConn (X ∪ Y) = ↑M.eConn X

theorem Matroid.eConn_add_nullity_add_nullity_dual {α : Type u_1} (M : Matroid α) (X : Set α) (hX : X ⊆ M.E := by aesop_mat) : ↑M.eConn X + M.nullity X + M✶.nullity X = X.encard

The slack term in the inequality λ(X) ≤ |X| is the sum of the nullity and conullity of X. This needs X ⊆ M.E, for instance in the case where X is a single non-element.

theorem Matroid.eConn_add_nullity_add_nullity_dual' {α : Type u_1} (M : Matroid α) (X : Set α) : ↑M.eConn X + M.nullity X + M✶.nullity X = X.encard + (X \ M.E).encard

theorem Matroid.eConn_eq_eRk_iff {α : Type u_1} {M : Matroid α} {X : Set α} (hX : ↑M.eConn X ≠ ⊤) (hXE : X ⊆ M.E := by aesop_mat) : ↑M.eConn X = M.eRk X ↔ M✶.Indep X

theorem Matroid.IsRkFinite.eConn_eq_eRk_iff {α : Type u_1} {M : Matroid α} {X : Set α} (h : M.IsRkFinite X) (hXE : X ⊆ M.E := by aesop_mat) : ↑M.eConn X = M.eRk X ↔ M✶.Indep X

theorem Matroid.eConn_eq_encard_iff' {α : Type u_1} {M : Matroid α} {X : Set α} (hX : ↑M.eConn X ≠ ⊤) : ↑M.eConn X = X.encard ↔ M.Indep X ∧ M.Coindep X

theorem Matroid.eConn_eq_encard_iff {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X.Finite) : ↑M.eConn X = X.encard ↔ M.Indep X ∧ M.Coindep X

theorem Matroid.eRk_add_eRk_dual_eq {α : Type u_1} (M : Matroid α) (X : Set α) (hX : X ⊆ M.E := by aesop_mat) : M.eRk X + M✶.eRk X = ↑M.eConn X + X.encard

theorem Matroid.Indep.eConn_eq {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) : ↑M.eConn I = M✶.eRk I

theorem Matroid.Indep.eConn_eq_zero_iff {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) : ↑M.eConn I = 0 ↔ I ⊆ M.coloops

theorem Matroid.Coindep.eConn_eq_zero_iff {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Coindep I) : ↑M.eConn I = 0 ↔ I ⊆ M.loops

theorem Matroid.Coindep.eConn_eq {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Coindep I) : ↑M.eConn I = M.eRk I

theorem Matroid.Spanning.eConn_eq {α : Type u_1} {M : Matroid α} {X : Set α} (h : M.Spanning X) : ↑M.eConn X = M.eRk (M.E \ X)

theorem Matroid.IsHyperplane.eConn_add_one_eq {α : Type u_1} {M : Matroid α} {H : Set α} (hH : M.IsHyperplane H) : ↑M.eConn H + 1 = M.eRk (M.E \ H)

theorem Matroid.IsCocircuit.eConn_add_one_eq {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCocircuit C) : ↑M.eConn C + 1 = M.eRk C

theorem Matroid.IsCircuit.eConn_add_one_eq {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) : ↑M.eConn C + 1 = M✶.eRk C

theorem Matroid.eConn_eq_eRk_compl_iff {α : Type u_1} {M : Matroid α} {X : Set α} (hX : ↑M.eConn X ≠ ⊤) (hXE : X ⊆ M.E := by aesop_mat) : ↑M.eConn X = M.eRk (M.E \ X) ↔ M.Spanning X

theorem Matroid.Indep.eConn_eq_encard_of_coindep {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) (hI' : M.Coindep I) : ↑M.eConn I = I.encard

theorem Matroid.eConn_lt_encard_iff' {α : Type u_1} {M : Matroid α} {X : Set α} (hX : ↑M.eConn X ≠ ⊤) : ↑M.eConn X < X.encard ↔ ¬M.Indep X ∨ ¬M.Coindep X

theorem Matroid.eConn_lt_encard_iff {α : Type u_1} {M : Matroid α} {X : Set α} (hX : ↑M.eConn X ≠ ⊤) (hXE : X ⊆ M.E := by aesop_mat) : ↑M.eConn X < X.encard ↔ M.Dep X ∨ M✶.Dep X

theorem Matroid.eConn_lt_encard_compl_iff {α : Type u_1} {M : Matroid α} {X : Set α} (hX : ↑M.eConn X ≠ ⊤) (hXE : X ⊆ M.E := by aesop_mat) : ↑M.eConn X < (M.E \ X).encard ↔ ¬M✶.Spanning X ∨ ¬M.Spanning X

theorem Matroid.eConn_lt_eRk_iff {α : Type u_1} {M : Matroid α} {X : Set α} (hX : ↑M.eConn X ≠ ⊤) (hXE : X ⊆ M.E := by aesop_mat) : ↑M.eConn X < M.eRk X ↔ ¬M.Spanning (M.E \ X)

theorem Matroid.eConn_lt_eRk_compl_iff {α : Type u_1} {M : Matroid α} {X : Set α} (hX : ↑M.eConn X ≠ ⊤) (hXE : X ⊆ M.E := by aesop_mat) : ↑M.eConn X < M.eRk (M.E \ X) ↔ ¬M.Spanning X

@[simp]

theorem Matroid.eConn_lt_top {α : Type u_1} (M : Matroid α) [M.RankFinite] (X : Set α) : ↑M.eConn X < ⊤

@[simp]

theorem Matroid.eConn_ne_top {α : Type u_1} (M : Matroid α) [M.RankFinite] (X : Set α) : ↑M.eConn X ≠ ⊤

@[simp]

theorem Matroid.eConn_lt_top' {α : Type u_1} (M : Matroid α) [M✶.RankFinite] (X : Set α) : ↑M.eConn X < ⊤

@[simp]

theorem Matroid.eConn_ne_top' {α : Type u_1} (M : Matroid α) [M✶.RankFinite] (X : Set α) : ↑M.eConn X ≠ ⊤

theorem Matroid.eConn_le_of_subset_of_subset_closure {α : Type u_1} {X Y : Set α} (M : Matroid α) (hXY : X ⊆ Y) (hYX : Y ⊆ M.closure X) : ↑M.eConn Y ≤ ↑M.eConn X

theorem Matroid.eConn_closure_le {α : Type u_1} (M : Matroid α) (X : Set α) : ↑M.eConn (M.closure X) ≤ ↑M.eConn X

@[simp]

theorem Matroid.eConn_disjointSum_left_eq {α : Type u_1} {M₁ M₂ : Matroid α} (hdj : Disjoint M₁.E M₂.E) : ↑(M₁.disjointSum M₂ hdj).eConn M₁.E = 0

@[simp]

theorem Matroid.eConn_disjointSum_right_eq {α : Type u_1} {M₁ M₂ : Matroid α} (hdj : Disjoint M₁.E M₂.E) : ↑(M₁.disjointSum M₂ hdj).eConn M₂.E = 0

theorem Matroid.eConn_eq_zero_iff_skew_compl {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X ⊆ M.E := by aesop_mat) : ↑M.eConn X = 0 ↔ M.Skew X (M.E \ X)

theorem Matroid.eConn_eq_zero_of_subset_loops {α : Type u_1} {M : Matroid α} {L : Set α} (hL : L ⊆ M.loops) : ↑M.eConn L = 0

theorem Matroid.eConn_eq_zero_of_subset_coloops {α : Type u_1} {M : Matroid α} {L : Set α} (hL : L ⊆ M.coloops) : ↑M.eConn L = 0

theorem Matroid.IsLoop.eConn_eq_zero {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsLoop e) : ↑M.eConn {e} = 0

theorem Matroid.IsColoop.eConn_eq_zero {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsColoop e) : ↑M.eConn {e} = 0

theorem Matroid.eConn_singleton_eq_zero_iff {α : Type u_1} {M : Matroid α} {e : α} (heM : e ∈ M.E) : ↑M.eConn {e} = 0 ↔ M.IsLoop e ∨ M.IsColoop e

theorem Matroid.eConn_inter_add_eConn_union_le {α : Type u_1} (M : Matroid α) (X Y : Set α) : ↑M.eConn (X ∩ Y) + ↑M.eConn (X ∪ Y) ≤ ↑M.eConn X + ↑M.eConn Y

Connectivity is submodular

theorem Matroid.eConn_submod {α : Type u_1} (M : Matroid α) (X Y : Set α) : ↑M.eConn (X ∩ Y) + ↑M.eConn (X ∪ Y) ≤ ↑M.eConn X + ↑M.eConn Y

Alias of Matroid.eConn_inter_add_eConn_union_le.

---

Connectivity is submodular

theorem Matroid.stronglyPreservable_eConn {α : Type u_1} : StronglyPreservable fun (M : Matroid α) (X : Set α) => ↑M.eConn X