isBridge_iff_adj_and_forall_walk_mem_edges

English

For edge e between v and w, IsBridge e is equivalent to e being an edge and every walk between v and w contains e.

Русский

Для ребра e между v и w условие IsBridge e эквивалентно тому, что e является ребром и для каждого хода между v и w e встречается в ребрах хода.

LaTeX

$$$ G.IsBridge s(v,w) \\iff G.Adj v w \\land \\forall p : G.Walk v w, s(v,w) \\in p.edges $$$

Lean4

theorem isBridge_iff_adj_and_forall_walk_mem_edges {v w : V} :
    G.IsBridge s(v, w) ↔ G.Adj v w ∧ ∀ p : G.Walk v w, s(v, w) ∈ p.edges :=
  by
  rw [isBridge_iff, and_congr_right']
  rw [reachable_delete_edges_iff_exists_walk, not_exists_not]

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