English
There exists a cycle in G that uses the edge s(v,w) if and only if there is an adjacency between v and w and a path from v to w that remains after deleting e, equivalently a cycle passing through e.
Русский
Существует цикл в графе G, использующий ребро s(v,w) тогда и только тогда, когда v и w смежны и существует путь от v до w, остающийся после удаления e (аналогично существованию цикла через e).
LaTeX
$$$ G.Adj v w \\land (G \\ fromEdgeSet {s(v,w)}).Reachable v w \\iff \\\\exists (u : V) (p : G.Walk u u), p.IsCycle \\land s(v,w) \\in p.edges $$$
Lean4
theorem adj_and_reachable_delete_edges_iff_exists_cycle {v w : V} :
G.Adj v w ∧ (G \ fromEdgeSet {s(v, w)}).Reachable v w ↔ ∃ (u : V) (p : G.Walk u u), p.IsCycle ∧ s(v, w) ∈ p.edges :=
by
classical
rw [reachable_delete_edges_iff_exists_walk]
constructor
· rintro ⟨h, p, hp⟩
refine ⟨w, Walk.cons h.symm p.toPath, ?_, ?_⟩
· apply Path.cons_isCycle
rw [Sym2.eq_swap]
intro h
cases hp (Walk.edges_toPath_subset p h)
· simp only [Sym2.eq_swap, Walk.edges_cons, List.mem_cons, true_or]
· rintro ⟨u, c, hc, he⟩
refine ⟨c.adj_of_mem_edges he, ?_⟩
by_contra! hb
have hb' : ∀ p : G.Walk w v, s(w, v) ∈ p.edges := by
intro p
simpa [Sym2.eq_swap] using hb p.reverse
have hvc : v ∈ c.support := Walk.fst_mem_support_of_mem_edges c he
refine
reachable_deleteEdges_iff_exists_cycle.aux hb' (c.rotate hvc) (hc.isTrail.rotate hvc) ?_
(Walk.start_mem_support _)
rwa [(Walk.rotate_edges c hvc).mem_iff, Sym2.eq_swap]
