reachable_delete_edges_iff_exists_walk

English

After deleting the edge e = s(v,w), v' can reach w' in the resulting graph iff there exists a walk p from v' to w' that does not use e.

Русский

После удаления ребра e = s(v,w) достижимо ли из v' в w' в полученном графе эквивалентно существованию обхода p от v' до w' без использования e.

LaTeX

$$$ (G \\ fromEdgeSet {s(v,w)}).Reachable v' w' \\iff \\exists p : G.Walk v' w', s(v,w) \\notin p.edges $$$

Lean4

theorem reachable_delete_edges_iff_exists_walk {v w v' w' : V} :
    (G \ fromEdgeSet {s(v, w)}).Reachable v' w' ↔ ∃ p : G.Walk v' w', s(v, w) ∉ p.edges :=
  by
  constructor
  · rintro ⟨p⟩
    use p.map (.ofLE (by simp))
    simp_rw [Walk.edges_map, List.mem_map, Hom.ofLE_apply, Sym2.map_id', id]
    rintro ⟨e, h, rfl⟩
    simpa using p.edges_subset_edgeSet h
  · rintro ⟨p, h⟩
    refine ⟨p.transfer _ fun e ep => ?_⟩
    simp only [edgeSet_sdiff, edgeSet_fromEdgeSet, edgeSet_sdiff_sdiff_isDiag]
    exact ⟨p.edges_subset_edgeSet ep, fun h' => h (h' ▸ ep)⟩

Похожие утверждения