V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
⊢ ¬Reachable (G \ fromEdgeSet {Quotient.mk (Sym2.Rel.setoid V) (v, w)}) v w ↔
    ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
⊢ IsBridge G (Quotient.mk (Sym2.Rel.setoid V) (v, w)) ↔
    Adj G v w ∧ ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
rw [isBridge_iff, and_congr_right']
no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
⊢ ¬Reachable (G \ fromEdgeSet {Quotient.mk (Sym2.Rel.setoid V) (v, w)}) v w ↔
    ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
rw [reachable_delete_edges_iff_exists_walk, not_exists_not]