isBridge_iff_mem_and_forall_cycle_notMem

English

An edge e is a bridge iff it is an edge and for all cycles p, not (p.edges contains e).

Русский

Ребро является мостом тогда и только тогда, когда оно является ребром и для всякого цикла p ребро e не встречается в его ребрах.

LaTeX

$$$ G.IsBridge e \\iff e \\text{ is an edge and } \\forall p : G.Walk, p.IsCycle \\rightarrow Not (p.edges e) $$$

Lean4

theorem isBridge_iff_mem_and_forall_cycle_notMem {e : Sym2 V} :
    G.IsBridge e ↔ e ∈ G.edgeSet ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → e ∉ p.edges :=
  Sym2.ind (fun _ _ => isBridge_iff_adj_and_forall_cycle_notMem) e

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