isAcyclic_iff_forall_adj_isBridge

English

A graph is acyclic iff every edge is a bridge: G.IsAcyclic iff ∀ v,w with G.Adj v w, the edge s(v,w) is a bridge.

Русский

Графа ацикличен тогда и только тогда, когда каждое ребро является мостом: G.IsAcyclic ⇔ ∀ вершины v,w с G.Adj v w, ребро s(v,w) является мостом.

LaTeX

$$$G.IsAcyclic \iff \forall ⦃v w : V⦄, G.Adj v w \Rightarrow G.IsBridge s(v, w)$$$

Lean4

theorem isAcyclic_iff_forall_adj_isBridge : G.IsAcyclic ↔ ∀ ⦃v w : V⦄, G.Adj v w → G.IsBridge s(v, w) :=
  by
  simp_rw [isBridge_iff_adj_and_forall_cycle_notMem]
  constructor
  · intro ha v w hvw
    apply And.intro hvw
    intro u p hp
    cases ha p hp
  · rintro hb v (_ | ⟨ha, p⟩) hp
    · exact hp.not_of_nil
    · apply (hb ha).2 _ hp
      rw [Walk.edges_cons]
      apply List.mem_cons_self

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