Vertical Separations

@[reducible, inline]

abbrev Matroid.Separation.IsVerticalSeparation {α : Type u_1} {M : Matroid α} (P : M.Separation) : Prop

A vertical separation is one with both sides nonspanning (or equivalently, with both sides coindependent).

Equations

• P.IsVerticalSeparation = Matroid.Separation.IsPredSeparation (fun (x : Bool) => Matroid.Coindep) P

@[simp]

theorem Matroid.Separation.isVerticalSeparation_symm_iff {α : Type u_1} {M : Matroid α} {P : M.Separation} : P.symm.IsVerticalSeparation ↔ P.IsVerticalSeparation

theorem Matroid.Separation.IsVerticalSeparation.symm {α : Type u_1} {M : Matroid α} {P : M.Separation} (hP : P.IsVerticalSeparation) : P.symm.IsVerticalSeparation

theorem Matroid.Separation.IsVerticalSeparation.of_symm {α : Type u_1} {M : Matroid α} {P : M.Separation} (hP : P.symm.IsVerticalSeparation) : P.IsVerticalSeparation

theorem Matroid.Separation.IsVerticalSeparation.isTutteSeparation {α : Type u_1} {M : Matroid α} {P : M.Separation} (h : P.IsVerticalSeparation) : P.IsTutteSeparation

theorem Matroid.Separation.isVerticalSeparation_iff_forall {α : Type u_1} {M : Matroid α} {P : M.Separation} : P.IsVerticalSeparation ↔ ∀ (b : Bool), M.Codep (P b)

theorem Matroid.Separation.isVerticalSeparation_iff {α : Type u_1} {M : Matroid α} {P : M.Separation} : P.IsVerticalSeparation ↔ M.Codep (P false) ∧ M.Codep (P true)

theorem Matroid.Separation.isVerticalSeparation_iff_forall_nonspanning {α : Type u_1} {M : Matroid α} {P : M.Separation} : P.IsVerticalSeparation ↔ ∀ (b : Bool), M.Nonspanning (P b)

theorem Matroid.Separation.not_isVerticalSeparation_iff_exists {α : Type u_1} {M : Matroid α} {P : M.Separation} : ¬P.IsVerticalSeparation ↔ ∃ (b : Bool), M.Coindep (P b)

theorem Matroid.Separation.not_isVerticalSeparation_iff_exists_spanning {α : Type u_1} {M : Matroid α} {P : M.Separation} : ¬P.IsVerticalSeparation ↔ ∃ (b : Bool), M.Spanning (P b)

theorem Matroid.Separation.IsVerticalSeparation.nonspanning {α : Type u_1} {M : Matroid α} {P : M.Separation} (h : P.IsVerticalSeparation) (b : Bool) : M.Nonspanning (P b)

theorem Matroid.Separation.IsVerticalSeparation.codep {α : Type u_1} {M : Matroid α} {P : M.Separation} (h : P.IsVerticalSeparation) (b : Bool) : M.Codep (P b)

theorem Matroid.Separation.isVerticalSeparation_iff_eRk {α : Type u_1} {M : Matroid α} {P : M.Separation} (h : P.eConn ≠ ⊤) : P.IsVerticalSeparation ↔ ∀ (b : Bool), P.eConn < M.eRk (P b)

theorem Matroid.Separation.isVerticalSeparation_iff_nullity_dual {α : Type u_1} {M : Matroid α} {P : M.Separation} : P.IsVerticalSeparation ↔ ∀ (b : Bool), 1 ≤ M✶.nullity (P b)

theorem Matroid.Separation.isVerticalSeparation_of_lt_lt {α : Type u_1} {M : Matroid α} {P : M.Separation} {b : Bool} (h : P.eConn < M.eRk (P b)) (h' : P.eConn < M.eRk (P !b)) : P.IsVerticalSeparation

theorem Matroid.Separation.IsVerticalSeparation.eRk_ge {α : Type u_1} {M : Matroid α} {P : M.Separation} (h : P.IsVerticalSeparation) (b : Bool) : P.eConn + 1 ≤ M.eRk (P b)

Cyclic Separations

@[reducible, inline]

abbrev Matroid.Separation.IsCyclicSeparation {α : Type u_1} {M : Matroid α} (P : M.Separation) : Prop

A cyclic separation is one with both sides dependent.

Equations

• P.IsCyclicSeparation = Matroid.Separation.IsPredSeparation (fun (x : Bool) => Matroid.Indep) P

@[simp]

theorem Matroid.Separation.isCyclicSeparation_symm_iff {α : Type u_1} {M : Matroid α} {P : M.Separation} : P.symm.IsCyclicSeparation ↔ P.IsCyclicSeparation

theorem Matroid.Separation.IsCyclicSeparation.of_symm {α : Type u_1} {M : Matroid α} {P : M.Separation} : P.symm.IsCyclicSeparation → P.IsCyclicSeparation

Alias of the forward direction of Matroid.Separation.isCyclicSeparation_symm_iff.

theorem Matroid.Separation.IsCyclicSeparation.symm {α : Type u_1} {M : Matroid α} {P : M.Separation} : P.IsCyclicSeparation → P.symm.IsCyclicSeparation

Alias of the reverse direction of Matroid.Separation.isCyclicSeparation_symm_iff.

theorem Matroid.Separation.IsVerticalSeparation.dual {α : Type u_1} {M : Matroid α} {P : M.Separation} (h : P.IsVerticalSeparation) : (P.induce M✶).IsCyclicSeparation

theorem Matroid.Separation.IsCyclicSeparation.dual {α : Type u_1} {M : Matroid α} {P : M.Separation} (h : P.IsCyclicSeparation) : (P.induce M✶).IsVerticalSeparation

theorem Matroid.Separation.IsCyclicSeparation.isTutteSeparation {α : Type u_1} {M : Matroid α} {P : M.Separation} (h : P.IsCyclicSeparation) : P.IsTutteSeparation

theorem Matroid.Separation.isCyclicSeparation_iff_forall {α : Type u_1} {M : Matroid α} {P : M.Separation} : P.IsCyclicSeparation ↔ ∀ (b : Bool), M.Dep (P b)

theorem Matroid.Separation.IsCyclicSeparation.dep {α : Type u_1} {M : Matroid α} {P : M.Separation} (h : P.IsCyclicSeparation) (b : Bool) : M.Dep (P b)

@[simp]

theorem Matroid.Separation.isCyclicSeparation_dual_iff {α : Type u_1} {M : Matroid α} {P : M.Separation} : (P.induce M✶).IsCyclicSeparation ↔ P.IsVerticalSeparation

@[simp]

theorem Matroid.Separation.isVerticalSeparation_dual_iff {α : Type u_1} {M : Matroid α} {P : M.Separation} : (P.induce M✶).IsVerticalSeparation ↔ P.IsCyclicSeparation

@[simp]

theorem Matroid.Separation.isCyclicSeparation_of_dual_iff {α : Type u_1} {M : Matroid α} {P : M✶.Separation} : (P.induce M).IsCyclicSeparation ↔ P.IsVerticalSeparation

@[simp]

theorem Matroid.Separation.isVerticalSeparation_ofDual_iff {α : Type u_1} {M : Matroid α} {P : M✶.Separation} : (P.induce M).IsVerticalSeparation ↔ P.IsCyclicSeparation

theorem Matroid.Separation.isCyclicSeparation_iff_eRk_dual {α : Type u_1} {M : Matroid α} {P : M.Separation} (h : P.eConn ≠ ⊤) : P.IsCyclicSeparation ↔ ∀ (b : Bool), P.eConn < M✶.eRk (P b)

theorem Matroid.Separation.isCyclicSeparation_iff_nullity {α : Type u_1} {M : Matroid α} {P : M.Separation} : P.IsCyclicSeparation ↔ ∀ (b : Bool), 1 ≤ M.nullity (P b)

theorem Matroid.Separation.not_isCyclicSeparation_iff {α : Type u_1} {M : Matroid α} {P : M.Separation} : ¬P.IsCyclicSeparation ↔ ∃ (b : Bool), M.Indep (P b)

theorem Matroid.Separation.IsCyclicSeparation.eRk_dual_ge {α : Type u_1} {M : Matroid α} {P : M.Separation} {b : Bool} (h : P.IsCyclicSeparation) : P.eConn + 1 ≤ M✶.eRk (P b)

Strict Separations

@[reducible, inline]

abbrev Matroid.Separation.IsStrictSeparation {α : Type u_1} {M : Matroid α} (P : M.Separation) : Prop

A strict separation is one where both sides are dependent and nonspanning.

Equations

• P.IsStrictSeparation = Matroid.Separation.IsPredSeparation (fun (x : Bool) (M : Matroid α) (X : Set α) => M.Indep X ∨ M.Coindep X) P

@[simp]

theorem Matroid.Separation.isStrictSeparation_symm_iff {α : Type u_1} {M : Matroid α} {P : M.Separation} : P.symm.IsStrictSeparation ↔ P.IsStrictSeparation

@[simp]

theorem Matroid.Separation.isStrictSeparation_dual_iff {α : Type u_1} {M : Matroid α} {P : M.Separation} : (P.induce M✶).IsStrictSeparation ↔ P.IsStrictSeparation

@[simp]

theorem Matroid.Separation.isStrictSeparation_ofDual_iff {α : Type u_1} {M : Matroid α} {P : M✶.Separation} : (P.induce M).IsStrictSeparation ↔ P.IsStrictSeparation

theorem Matroid.Separation.IsStrictSeparation.of_dual {α : Type u_1} {M : Matroid α} {P : M.Separation} : (P.induce M✶).IsStrictSeparation → P.IsStrictSeparation

Alias of the forward direction of Matroid.Separation.isStrictSeparation_dual_iff.

theorem Matroid.Separation.IsStrictSeparation.dual {α : Type u_1} {M : Matroid α} {P : M.Separation} : P.IsStrictSeparation → (P.induce M✶).IsStrictSeparation

Alias of the reverse direction of Matroid.Separation.isStrictSeparation_dual_iff.

theorem Matroid.Separation.IsStrictSeparation.isCyclicSeparation {α : Type u_1} {M : Matroid α} {P : M.Separation} (h : P.IsStrictSeparation) : P.IsCyclicSeparation

theorem Matroid.Separation.IsStrictSeparation.isVerticalSeparation {α : Type u_1} {M : Matroid α} {P : M.Separation} (h : P.IsStrictSeparation) : P.IsVerticalSeparation

theorem Matroid.Separation.IsStrictSeparation.isTutteSeparation {α : Type u_1} {M : Matroid α} {P : M.Separation} (h : P.IsStrictSeparation) : P.IsTutteSeparation

theorem Matroid.Separation.isStrictSeparation_iff {α : Type u_1} {M : Matroid α} {P : M.Separation} : P.IsStrictSeparation ↔ (∀ (b : Bool), M.Dep (P b)) ∧ ∀ (b : Bool), M.Codep (P b)

theorem Matroid.Separation.not_isStrictSeparation_iff {α : Type u_1} {M : Matroid α} {P : M.Separation} : ¬P.IsStrictSeparation ↔ ∃ (b : Bool), M.Indep (P b) ∨ M.Coindep (P b)

theorem Matroid.Separation.isStrictSeparation_iff' {α : Type u_1} {M : Matroid α} {P : M.Separation} : P.IsStrictSeparation ↔ (∀ (b : Bool), M.Dep (P b)) ∧ ∀ (b : Bool), M.Nonspanning (P b)

theorem Matroid.Separation.IsStrictSeparation.dep {α : Type u_1} {M : Matroid α} {P : M.Separation} (h : P.IsStrictSeparation) (b : Bool) : M.Dep (P b)

theorem Matroid.Separation.IsStrictSeparation.codep {α : Type u_1} {M : Matroid α} {P : M.Separation} (h : P.IsStrictSeparation) (b : Bool) : M.Codep (P b)

theorem Matroid.Separation.IsStrictSeparation.nonspanning {α : Type u_1} {M : Matroid α} {P : M.Separation} (h : P.IsStrictSeparation) (b : Bool) : M.Nonspanning (P b)

theorem Matroid.Separation.IsStrictSeparation.encard_ge {α : Type u_1} {M : Matroid α} {P : M.Separation} {b : Bool} (h : P.IsStrictSeparation) : P.eConn + 2 ≤ (P b).encard

theorem Matroid.Separation.isStrictSeparation_iff_eRk {α : Type u_1} {M : Matroid α} {P : M.Separation} (hP : P.eConn ≠ ⊤) : P.IsStrictSeparation ↔ (∀ (b : Bool), P.eConn < M.eRk (P b)) ∧ ∀ (b : Bool), P.eConn < M✶.eRk (P b)

theorem Matroid.Separation.isTutteSeparation_iff_isStrictSeparation_of_zero {α : Type u_1} {M : Matroid α} {P : M.Separation} (hP : P.eConn = 0) : P.IsTutteSeparation ↔ P.IsStrictSeparation ∨ (∀ (b : Bool), (P b).Nonempty) ∧ ∃ (b : Bool), P b ⊆ M.loops ∨ P b ⊆ M.coloops

A Tutte separation with connectivity zero is either strict, or has one side only loops or coloops.

theorem Matroid.Dep.ofSetSep_isTutteSeparation_of_nonspanning {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.Dep X) (hX' : M.Nonspanning X) (b : Bool) : (M.ofSetSep X b ⋯).IsTutteSeparation

theorem Matroid.Nonspanning.ofSetSep_isVerticalSeparation {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.Nonspanning X) (hXc : M.Nonspanning (M.E \ X)) (b : Bool) : (M.ofSetSep X b ⋯).IsVerticalSeparation

theorem Matroid.Codep.ofSetSep_isVerticalSeparation {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.Codep X) (hXc : M.Nonspanning X) (b : Bool) : (M.ofSetSep X b ⋯).IsVerticalSeparation

theorem Matroid.Codep.ofSetSep_isTutteSeparation_of_dep_compl {α : Type u_1} {M : Matroid α} {X : Set α} {b : Bool} (hX : M.Codep X) (hXc : M.Dep (M.E \ X)) : (M.ofSetSep X b ⋯).IsTutteSeparation

theorem Matroid.Dep.ofSetSep_isCyclicSeparation {α : Type u_1} {M : Matroid α} {X : Set α} {b : Bool} (hX : M.Dep X) (hXc : M.Dep (M.E \ X)) : (M.ofSetSep X b ⋯).IsCyclicSeparation

theorem Matroid.Dep.ofSetSep_isStrictSeparation {α : Type u_1} {M : Matroid α} {X : Set α} {b : Bool} (hX : M.Dep X) (hns : M.Nonspanning X) (hXc : M.Dep (M.E \ X)) (hXsc : M.Nonspanning (M.E \ X)) : (M.ofSetSep X b ⋯).IsStrictSeparation

theorem Matroid.TutteConnected.not_isCyclicSeparation {α : Type u_1} {M : Matroid α} {k : ℕ∞} {P : M.Separation} (h : M.TutteConnected (k + 1)) (hP : P.eConn + 1 ≤ k) : ¬P.IsCyclicSeparation

theorem Matroid.TutteConnected.not_isVerticalSeparation {α : Type u_1} {M : Matroid α} {k : ℕ∞} {P : M.Separation} (h : M.TutteConnected (k + 1)) (hP : P.eConn + 1 ≤ k) : ¬P.IsVerticalSeparation

theorem Matroid.exists_strong_or_small_of_not_tutteConnected {α : Type u_1} {M : Matroid α} {k : ℕ∞} (h : ¬M.TutteConnected (k + 1)) (b : Bool) : ∃ (P : M.Separation), P.eConn + 1 ≤ k ∧ P.IsTutteSeparation ∧ (P.IsStrictSeparation ∨ (P b).encard ≤ k ∧ (M.Indep (P b) ∧ M.IsHyperplane (P !b) ∨ M.IsCircuit (P b) ∧ M.Spanning (P !b)))

In a matroid that isn't (k + 1)-connected, there is either a strong separation, or a separation arising from a small circuit or cocircuit.

Vertical Connectivity

def Matroid.VerticallyConnected {α : Type u_1} (M : Matroid α) (k : ℕ∞) : Prop

Equations

• M.VerticallyConnected = M.NumConnected Matroid.Coindep

theorem Matroid.VerticallyConnected.mono {α : Type u_1} {M : Matroid α} {j k : ℕ∞} (h : M.VerticallyConnected k) (hjk : j ≤ k) : M.VerticallyConnected j

theorem Matroid.VerticallyConnected.mono' {α : Type u_1} {M : Matroid α} {j k : ℕ∞} (hjk : j ≤ k) (h : M.VerticallyConnected k) : M.VerticallyConnected j

theorem Matroid.TutteConnected.verticallyConnected {α : Type u_1} {M : Matroid α} {k : ℕ∞} (h : M.TutteConnected k) : M.VerticallyConnected k

theorem Matroid.not_verticallyConnected_iff_exists {α : Type u_1} {M : Matroid α} {k : ℕ∞} : ¬M.VerticallyConnected (k + 1) ↔ ∃ (P : M.Separation), P.eConn + 1 ≤ k ∧ P.IsVerticalSeparation

theorem Matroid.verticallyConnected_iff_forall {α : Type u_1} {M : Matroid α} {k : ℕ∞} : M.VerticallyConnected (k + 1) ↔ ∀ (P : M.Separation), P.eConn + 1 ≤ k → ¬P.IsVerticalSeparation

theorem Matroid.VerticallyConnected.exists_eRk_eq {α : Type u_1} {M : Matroid α} {k : ℕ∞} {P : M.Separation} (h : M.VerticallyConnected (k + 1)) (hP : P.eConn + 1 ≤ k) : ∃ (i : Bool), M.eRk (P i) = P.eConn

theorem Matroid.verticallyConnected_iff_forall_exists_eRk_le {α : Type u_1} {M : Matroid α} {k : ℕ∞} (hk : k ≠ ⊤) : M.VerticallyConnected (k + 1) ↔ ∀ (P : M.Separation), P.eConn + 1 ≤ k → ∃ (i : Bool), M.eRk (P i) ≤ P.eConn

theorem Matroid.VerticallyConnected.exists_spanning {α : Type u_1} {M : Matroid α} {k : ℕ∞} {P : M.Separation} (h : M.VerticallyConnected (k + 1)) (hP : P.eConn + 1 ≤ k) : ∃ (i : Bool), M.Spanning (P i)

theorem Matroid.VerticallyConnected.exists_coindep {α : Type u_1} {M : Matroid α} {k : ℕ∞} {P : M.Separation} (h : M.VerticallyConnected (k + 1)) (hP : P.eConn + 1 ≤ k) : ∃ (i : Bool), M.Coindep (P i)

theorem Matroid.Separation.IsVerticalSeparation.not_verticallyConnected {α : Type u_1} {M : Matroid α} {P : M.Separation} (hP : P.IsVerticalSeparation) : ¬M.VerticallyConnected (P.eConn + 1 + 1)

theorem Matroid.VerticallyConnected.not_isVerticalSeparation {α : Type u_1} {M : Matroid α} {k : ℕ∞} {P : M.Separation} (h : M.VerticallyConnected (k + 1)) (hP : P.eConn + 1 ≤ k) : ¬P.IsVerticalSeparation

theorem Matroid.VerticallyConnected.compl_spanning_of_nonspanning_of_eConn_le {α : Type u_1} {M : Matroid α} {k : ℕ∞} {X : Set α} (h : M.VerticallyConnected (k + 1)) (hX : M.Nonspanning X) (hconn : ↑M.eConn X + 1 ≤ k) : M.Spanning (M.E \ X)

theorem Matroid.verticallyConnected_top_iff {α : Type u_1} {M : Matroid α} : M.VerticallyConnected ⊤ ↔ ∀ X ⊆ M.E, M.Spanning X ∨ M.Spanning (M.E \ X)

@[simp]

theorem Matroid.verticallyConnected_loopyOn {α : Type u_1} (E : Set α) (k : ℕ∞) : (loopyOn E).VerticallyConnected k

@[simp]

theorem Matroid.verticallyConnected_zero {α : Type u_1} (M : Matroid α) : M.VerticallyConnected 0

@[simp]

theorem Matroid.verticallyConnected_one {α : Type u_1} (M : Matroid α) : M.VerticallyConnected 1

@[simp]

theorem Matroid.verticallyConnected_of_le_one {α : Type u_1} {k : ℕ∞} (M : Matroid α) (hk : k ≤ 1) : M.VerticallyConnected k

@[simp]

theorem Matroid.verticallyConnected_freeOn_iff {α : Type u_1} (E : Set α) (k : ℕ∞) : (freeOn E).VerticallyConnected (k + 1) ↔ E.Subsingleton ∨ k = 0

theorem Matroid.verticallyConnected_iff_seqConnected {α : Type u_1} {M : Matroid α} {k : ℕ∞} : M.VerticallyConnected (k + 1) ↔ M.SeqConnected (fun (M : Matroid α) => M✶.nullity) ({i : ℕ∞ | k < i + 1}.indicator ⊤)

Cyclic connectivity

def Matroid.CyclicallyConnected {α : Type u_1} (M : Matroid α) (k : ℕ∞) : Prop

Equations

• M.CyclicallyConnected k = M.NumConnected Matroid.Indep k

theorem Matroid.CyclicallyConnected.dual_verticallyConnected {α : Type u_1} {M : Matroid α} {k : ℕ∞} (h : M.CyclicallyConnected k) : M✶.VerticallyConnected k

theorem Matroid.VerticallyConnected.dual_cyclicallyConnected {α : Type u_1} {M : Matroid α} {k : ℕ∞} (h : M.VerticallyConnected k) : M✶.CyclicallyConnected k

@[simp]

theorem Matroid.verticallyConnected_dual_iff {α : Type u_1} {M : Matroid α} {k : ℕ∞} : M✶.VerticallyConnected k ↔ M.CyclicallyConnected k

@[simp]

theorem Matroid.cyclicallyConnected_dual_iff {α : Type u_1} {M : Matroid α} {k : ℕ∞} : M✶.CyclicallyConnected k ↔ M.VerticallyConnected k

theorem Matroid.CyclicallyConnected.mono {α : Type u_1} {M : Matroid α} {j k : ℕ∞} (h : M.CyclicallyConnected k) (hjk : j ≤ k) : M.CyclicallyConnected j

theorem Matroid.CyclicallyConnected.mono' {α : Type u_1} {M : Matroid α} {j k : ℕ∞} (hjk : j ≤ k) (h : M.CyclicallyConnected k) : M.CyclicallyConnected j

theorem Matroid.TutteConnected.cyclicallyConnected {α : Type u_1} {M : Matroid α} {k : ℕ∞} (h : M.TutteConnected k) : M.CyclicallyConnected k

theorem Matroid.not_cyclicallyConnected_iff_exists {α : Type u_1} {M : Matroid α} {k : ℕ∞} : ¬M.CyclicallyConnected (k + 1) ↔ ∃ (P : M.Separation), P.eConn + 1 ≤ k ∧ P.IsCyclicSeparation

theorem Matroid.cyclicallyConnected_iff_forall {α : Type u_1} {M : Matroid α} {k : ℕ∞} : M.CyclicallyConnected (k + 1) ↔ ∀ (P : M.Separation), P.eConn + 1 ≤ k → ¬P.IsCyclicSeparation

theorem Matroid.cyclicallyConnected_iff_seqConnected {α : Type u_1} {M : Matroid α} {k : ℕ∞} : M.CyclicallyConnected (k + 1) ↔ M.SeqConnected nullity ({i : ℕ∞ | k < i + 1}.indicator ⊤)

theorem Matroid.Separation.IsCyclicSeparation.not_cyclicallyConnected {α : Type u_1} {M : Matroid α} {P : M.Separation} (hP : P.IsCyclicSeparation) : ¬M.CyclicallyConnected (P.eConn + 1 + 1)

theorem Matroid.CyclicallyConnected.not_isCyclicSeparation {α : Type u_1} {M : Matroid α} {k : ℕ∞} {P : M.Separation} (h : M.CyclicallyConnected k) (hP : P.eConn + 1 + 1 ≤ k) : ¬P.IsCyclicSeparation

theorem Matroid.CyclicallyConnected.compl_indep_of_dep_of_eConn_le {α : Type u_1} {M : Matroid α} {k : ℕ∞} {X : Set α} (h : M.CyclicallyConnected (k + 1)) (hX : M.Dep X) (hXconn : ↑M.eConn X + 1 ≤ k) : M.Indep (M.E \ X)

@[simp]

theorem Matroid.cyclicallyConnected_zero {α : Type u_1} (M : Matroid α) : M.CyclicallyConnected 0

@[simp]

theorem Matroid.cyclicallyConnected_one {α : Type u_1} (M : Matroid α) : M.CyclicallyConnected 1

@[simp]

theorem Matroid.cyclicallyConnected_of_le_one {α : Type u_1} {k : ℕ∞} (M : Matroid α) (hk : k ≤ 1) : M.CyclicallyConnected k

theorem Matroid.IsLoop.not_tutteConnected {α : Type u_1} {M : Matroid α} {k : ℕ∞} {e : α} (he : M.IsLoop e) (hME : M.E.Nontrivial) (hk : 1 ≤ k) : ¬M.TutteConnected (k + 1)

theorem Matroid.IsColoop.not_tutteConnected {α : Type u_1} {M : Matroid α} {k : ℕ∞} {e : α} (he : M.IsColoop e) (hME : M.E.Nontrivial) (hk : 1 ≤ k) : ¬M.TutteConnected (k + 1)

theorem Matroid.CyclicallyConnected.le_girth {α : Type u_1} {M : Matroid α} {k : ℕ∞} (h : M.CyclicallyConnected k) (hlt : k ≤ M✶.eRank) : k ≤ M.girth

This needs the lower bound on co-rank; otherwise an extension of a large free matroid by a loop would be a counterexample for any k.

theorem Matroid.VerticallyConnected.tutteConnected_of_girth_ge {α : Type u_1} {M : Matroid α} {k : ℕ∞} (h : M.VerticallyConnected k) (hk : k ≠ ⊤) (h_girth : k ≤ M.girth) : M.TutteConnected k

theorem Matroid.tutteConnected_iff_verticallyConnected_girth {α : Type u_1} {M : Matroid α} {k : ℕ∞} (hlt : 2 * k < M.E.encard + 1) : M.TutteConnected (k + 1) ↔ M.VerticallyConnected (k + 1) ∧ k + 1 ≤ M.girth

This needs the strict inequality in the hypothesis, since nothing like this can be true for k = ⊤. This is also false for matroids like U₂,₅ if there is no lower bound on size.

theorem Matroid.tutteConnected_iff_verticallyConnected_cyclicallyConnected {α : Type u_1} {M : Matroid α} {k : ℕ∞} (hlt : 2 * k < M.E.encard) : M.TutteConnected (k + 1) ↔ M.VerticallyConnected (k + 1) ∧ M.CyclicallyConnected (k + 1)

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

theorem Matroid.VerticallyConnected.contract_of_top {α : Type u_1} {M : Matroid α} (h : M.VerticallyConnected ⊤) (C : Set α) : (M.contract C).VerticallyConnected ⊤

theorem Matroid.VerticallyConnected.of_isSpanningRestriction {α : Type u_1} {M N : Matroid α} {k : ℕ∞} (h : N.VerticallyConnected k) (hNM : N.IsSpanningRestriction M) : M.VerticallyConnected k

theorem Matroid.VerticallyConnected.of_simplifies {α : Type u_1} {M N : Matroid α} {k : ℕ∞} (h : M.VerticallyConnected k) (hNM : N.Simplifies M) : N.VerticallyConnected k

theorem Matroid.Simplifies.verticallyConnected_iff {α : Type u_1} {M N : Matroid α} {k : ℕ∞} (hNM : N.Simplifies M) : N.VerticallyConnected k ↔ M.VerticallyConnected k

theorem Matroid.verticallyConnected_two_iff {α : Type u_1} {M : Matroid α} : M.VerticallyConnected 2 ↔ M.removeLoops.TutteConnected 2

theorem Matroid.IsSimplification.verticallyConnected_three_iff {α : Type u_1} {M N : Matroid α} (hNM : N.IsSimplification M) : M.VerticallyConnected 3 ↔ N.TutteConnected 3

M is vertically 3-connected if and only if its simplification is 3-connected.

theorem Matroid.IsSimplification.tutteConnected_of_verticallyConnected_three {α : Type u_1} {M N : Matroid α} (hNM : N.IsSimplification M) (hM : M.VerticallyConnected 3) : N.TutteConnected 3

@[simp]

theorem Matroid.verticallyConnected_three_iff {α : Type u_1} {M : Matroid α} [M.Simple] : M.VerticallyConnected 3 ↔ M.TutteConnected 3

theorem Matroid.TutteConnected.contract {α : Type u_1} {M : Matroid α} {k : ℕ∞} {C : Set α} (h : M.TutteConnected (k + M.eRk C + 1)) (hnt : 2 * (k + M.eRk C) < M.E.encard + 1) : (M.contract C).TutteConnected (k + 1)

theorem Matroid.TutteConnected.delete {α : Type u_1} {M : Matroid α} {k : ℕ∞} {D : Set α} (h : M.TutteConnected (k + M✶.eRk D + 1)) (hnt : 2 * (k + M✶.eRk D) < M.E.encard + 1) : (M.delete D).TutteConnected (k + 1)

theorem Matroid.TutteConnected.contractElem {α : Type u_1} {M : Matroid α} {k : ℕ∞} (h : M.TutteConnected (k + 1)) (hnt : 2 * k < M.E.encard + 1) (e : α) : (M.contract {e}).TutteConnected k

theorem Matroid.TutteConnected.deleteElem {α : Type u_1} {M : Matroid α} {k : ℕ∞} (h : M.TutteConnected (k + 1)) (hnt : 2 * k < M.E.encard + 1) (e : α) : (M.delete {e}).TutteConnected k

theorem Matroid.TutteConnected.connected_deleteElem {α : Type u_1} {M : Matroid α} (h : M.TutteConnected (2 + 1)) (h4 : 4 ≤ M.E.encard) (e : α) : (M.delete {e}).Connected

theorem Matroid.TutteConnected.connected_contractElem {α : Type u_1} {M : Matroid α} (h : M.TutteConnected (2 + 1)) (h4 : 4 ≤ M.E.encard) (e : α) : (M.contract {e}).Connected

theorem Matroid.TutteConnected.removeElem {α : Type u_1} {M : Matroid α} {k : ℕ∞} (h : M.TutteConnected (k + 1)) (hnt : 2 * k < M.E.encard + 1) (b : Bool) (e : α) : (M.remove b {e}).TutteConnected k

theorem Matroid.TutteConnected.of_isMinor {α : Type u_1} {M N : Matroid α} {k t : ℕ∞} (h : M.TutteConnected (k + t + 1)) (hNM : N ≤m M) (hNT : (M.E \ N.E).encard ≤ t) (hk : 2 * (k + t) < M.E.encard + 1) : N.TutteConnected (k + 1)

theorem Matroid.TutteConnected.notMem_closure_dual_of_separation_contractElem {α : Type u_1} {M : Matroid α} {k : ℕ∞} {e : α} (h : M.TutteConnected (k + 1)) {P : (M.contract {e}).Separation} (hPk : P.eConn + 1 ≤ k) (hP : P.IsTutteSeparation) (i : Bool) : e ∉ M✶.closure (P i)

theorem Matroid.TutteConnected.mem_closure_of_separation_contractElem {α : Type u_1} {M : Matroid α} {k : ℕ∞} {e : α} (h : M.TutteConnected (k + 1)) {P : (M.contract {e}).Separation} (hPk : P.eConn + 1 ≤ k) (hP : P.IsTutteSeparation) (i : Bool) : e ∈ M.closure (P i)

theorem Matroid.TutteConnected.mem_closure_bDual_iff_of_separation_removeElem {α : Type u_1} {M : Matroid α} {k : ℕ∞} {e : α} (h : M.TutteConnected (k + 1)) {b c : Bool} {P : (M.remove b {e}).Separation} (hPk : P.eConn + 1 ≤ k) (hP : P.IsTutteSeparation) (i : Bool) : e ∈ (M.bDual c).closure (P i) ↔ (b != c) = true

If M is a (k + 1)-connected matroid, and P is a k-separation in a single removal of M, then we know which sides of P span the removed element in M, both in the primal and the dual.

theorem Matroid.TutteConnected.mem_closure_dual_of_separation_deleteElem {α : Type u_1} {M : Matroid α} {k : ℕ∞} {e : α} (h : M.TutteConnected (k + 1)) {P : (M.delete {e}).Separation} (hPk : P.eConn + 1 ≤ k) (hP : P.IsTutteSeparation) (i : Bool) : e ∈ M✶.closure (P i)

theorem Matroid.TutteConnected.notMem_closure_of_separation_deleteElem {α : Type u_1} {M : Matroid α} {k : ℕ∞} {e : α} (h : M.TutteConnected (k + 1)) {P : (M.delete {e}).Separation} (hPk : P.eConn + 1 ≤ k) (hP : P.IsTutteSeparation) (i : Bool) : e ∉ M.closure (P i)

theorem Matroid.TutteConnected.faithful_of_tutteConnected_remove {α : Type u_1} {M : Matroid α} {k : ℕ∞} {b : Bool} {e : α} (h : M.TutteConnected (k + 1)) (hN : (M.remove b {e}).TutteConnected (k + 1)) (P : M.Separation) (hP : P.eConn ≤ k) (hP' : ∀ (i : Bool), k < (P i).encard) : P.Faithful (M.remove b {e})

theorem Matroid.TutteConnected.faithful_of_tutteConnected_delete {α : Type u_1} {M : Matroid α} {k : ℕ∞} {e : α} (h : M.TutteConnected (k + 1)) (hN : (M.delete {e}).TutteConnected (k + 1)) (P : M.Separation) (hP : P.eConn ≤ k) (hP' : ∀ (i : Bool), k < (P i).encard) : P.Faithful (M.delete {e})

If M and M ＼ {e} are (k + 1)-connected, then every k-separation of M with sides of size greater than k is faithful to M ＼ {e}.

theorem Matroid.TutteConnected.faithful_of_tutteConnected_contract {α : Type u_1} {M : Matroid α} {k : ℕ∞} {e : α} (h : M.TutteConnected (k + 1)) (hN : (M.contract {e}).TutteConnected (k + 1)) (P : M.Separation) (hP : P.eConn ≤ k) (hP' : ∀ (i : Bool), k < (P i).encard) : P.Faithful (M.contract {e})

If M and M ／ {e} are (k + 1)-connected, then every k-separation of M with sides of size greater than k is faithful to M ／ {e}.