Edge-connectivity

[YaelDillies]

Edge-connectivity is an important concept in graph theory, showing up among other things in the statement of Menger's theorem.

Your task, if you accept it, is to define

def IsEdgeReachable (k : ℕ) (u v : V) : Prop :=
  ∀ ⦃s : Set (Sym2 V)⦄, s.encard < k → (G.deleteEdges s).Reachable u v

def IsEdgeConnected (k : ℕ) : Prop := ∀ u v, G.IsEdgeReachable k u v

and prove basic facts such as

@[simp] lemma IsEdgeReachable.rfl : G.IsEdgeReachable k u u := sorry

@[simp] lemma IsEdgeReachable.trans (huv : G.IsEdgeReachable k u v) (hvw : G.IsEdgeReachable k v w) :
      G.IsEdgeReachable k u w := sorry

@[simp] lemma IsEdgeReachable.mono (hkl : k ≤ l) :
    G.IsEdgeReachable l u v → G.IsEdgeReachable k u v := sorry

@[simp] lemma IsEdgeReachable.zero : G.IsEdgeReachable 0 u v := sorry
@[simp] lemma isEdgeReachable_one : G.IsEdgeReachable 1 u v ↔ G.Reachable u v := sorry

lemma isEdgeReachable_succ :
    G.IsEdgeReachable (k + 1) u v ↔ ∀ e, (G.deleteEdges {e}).IsEdgeReachable k u v := sorry

lemma isEdgeConnected_succ :
    G.IsEdgeConnected (k + 1) ↔ ∀ e, (G.deleteEdges {e}).IsEdgeConnected k := sorry

and possibly more lemmas relating G.IsEdgeConnected 2 and G.IsAcyclic. Finally, you could replace the (G.deleteEdges {e}).Reachable u v assumptions in Combinatorics.SimpleGraph.Connectivity.Connected with G.IsEdgeReachable 2 u v.

[Shiney]

Not sure I'll get round to doing all of this but the definition of IsEdgeConnected should be

def IsEdgeConnected (k : ℕ) : Prop := ∀ u v, G.IsEdgeReachable k u v

or it won't compile

[YaelDillies]

Thanks for the report, fixed.

[Shiney]

Right I've managed to prove all but one of these so far so probably worth me claiming it now

[Shiney]

Right isEdgeReachable_succ is impossible as stated because its not true for k =0 as all graphs are 0-edge-connected regardless of what edges are deleted. @YaelDillies do you think this is somehow a problem with how edge reachability and edge connectedness are formalised above? Or do you think we just need to add a k >0 hypothesis to the last two?

[Shiney]

Also the acyclic implies not 2 edge connected is also messy because you need to add an assumption that there are at least 2 elements of the graph

[YaelDillies]

Or do you think we just need to add a k >0 hypothesis to the last two?

Just assume k non-zero for now. I don't think there's a satisfying definition of 0-edge connected that would avoid this

Also the acyclic implies not 2 edge connected is also messy because you need to add an assumption that there are at least 2 elements of the graph

This seems fine. Assume Nontrivial V and you're good.