isAcyclic_iff_forall_edge_isBridge

English

A graph is acyclic iff every edge in its edge set is a bridge.

Русский

Графа ацикличен тогда и только тогда, когда каждое ребро в его множестве ребер является мостом.

LaTeX

$$$G.IsAcyclic \iff ∀ e \in G.edgeSet, G.IsBridge e$$$

Lean4

theorem isAcyclic_iff_forall_edge_isBridge : G.IsAcyclic ↔ ∀ ⦃e⦄, e ∈ (G.edgeSet) → G.IsBridge e := by
  simp [isAcyclic_iff_forall_adj_isBridge, Sym2.forall]

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