isBridge_iff — Mathlib

English

An edge e = s(u,v) is a bridge exactly when u and v are adjacent and removing e disconnects u and v.

Русский

Ребро e = s(u,v) является мостом тогда и только тогда, когда u и v смежны, и удаление e разделяет их.

LaTeX

$$$ G.IsBridge s(u,v) \\iff G.Adj u v \\\\land \\\\lnot (G \\\\ fromEdgeSet {s(u,v)}).Reachable u v $$$

Lean4

theorem isBridge_iff {u v : V} : G.IsBridge s(u, v) ↔ G.Adj u v ∧ ¬(G \ fromEdgeSet {s(u, v)}).Reachable u v :=
  Iff.rfl

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