English
If an edge is present in G and G is a cycle, deleting that edge leaves its endpoints still reachable.
Русский
Если ребро присутствует в G и G содержит цикл, удаление этого ребра сохраняет достижимость конечных вершин.
LaTeX
$$(G.Adj v w) → (G.IsCycles → (G.deleteEdges {s(v,w)}).Reachable v w)$$
Lean4
theorem reachable_deleteEdges [Finite V] (hadj : G.Adj v w) (hcyc : G.IsCycles) :
(G.deleteEdges {s(v, w)}).Reachable v w :=
by
have : fromEdgeSet {s(v, w)} = hadj.toWalk.toSubgraph.spanningCoe :=
by
simp only [Walk.toSubgraph, singletonSubgraph_le_iff, subgraphOfAdj_verts, Set.mem_insert_iff,
Set.mem_singleton_iff, or_true, sup_of_le_left]
exact (Subgraph.spanningCoe_subgraphOfAdj hadj).symm
rw [show G.deleteEdges {s(v, w)} = G \ fromEdgeSet {s(v, w)} from by rfl]
exact this ▸ (hcyc.reachable_sdiff_toSubgraph_spanningCoe hadj.toWalk (Walk.IsPath.of_adj hadj)).symm
