Connectivity of the factors of a one-vertex cut

The two induced graphs associated with a one-vertex cut inherit connectivity from the ambient graph.

theorem Utilities.OneVertexCut.graph_connected_left_of_connected {K : CFGraph} (cut : OneVertexCut K) (hK : graphConnected K) : graphConnected cut.leftGraph

def Utilities.OneVertexCut.swap {K : CFGraph} (cut : OneVertexCut K) : OneVertexCut K

The same cut with its two factors exchanged.

Equations

• cut.swap = { left := cut.right, right := cut.left, glue := cut.glue, glue_mem_left := ⋯, glue_mem_right := ⋯, vertex_cover := ⋯, only_overlap := ⋯, no_cross := ⋯ }

@[simp]

theorem Utilities.OneVertexCut.swap_leftGraph {K : CFGraph} (cut : OneVertexCut K) : cut.swap.leftGraph = cut.rightGraph

@[simp]

theorem Utilities.OneVertexCut.swap_rightGraph {K : CFGraph} (cut : OneVertexCut K) : cut.swap.rightGraph = cut.leftGraph

@[simp]

theorem Utilities.OneVertexCut.swap_leftGlue {K : CFGraph} (cut : OneVertexCut K) : cut.swap.leftGlue = cut.rightGlue

@[simp]

theorem Utilities.OneVertexCut.swap_rightGlue {K : CFGraph} (cut : OneVertexCut K) : cut.swap.rightGlue = cut.leftGlue

theorem Utilities.OneVertexCut.graph_connected_right_of_connected {K : CFGraph} (cut : OneVertexCut K) (hK : graphConnected K) : graphConnected cut.rightGraph

theorem Utilities.OneVertexCut.graph_connected_factors {K : CFGraph} (cut : OneVertexCut K) (hK : graphConnected K) : graphConnected cut.leftGraph ∧ graphConnected cut.rightGraph

theorem Utilities.OneVertexCut.graph_connected_iff_factors {K : CFGraph} (cut : OneVertexCut K) : graphConnected K ↔ graphConnected cut.leftGraph ∧ graphConnected cut.rightGraph