reachable_sdiff_toSubgraph_spanningCoe

English

For a cycle in G, removing a subgraph via sdiff preserves reachability relationships in spanningCoe.

Русский

Для цикла в G удаление подграфа через sdiff сохраняет достижимость в spanningCoe.

LaTeX

$$G.IsCycles → (G.sdiff.sdiff G p.toSubgraph.spanningCoe).Reachable w v$$

Lean4

theorem reachable_sdiff_toSubgraph_spanningCoe [Finite V] {v w : V} (hcyc : G.IsCycles) (p : G.Walk v w)
    (hp : p.IsPath) : (G \ p.toSubgraph.spanningCoe).Reachable w v :=
  by
  have : Fintype V := Fintype.ofFinite V
  exact reachable_sdiff_toSubgraph_spanningCoe_aux hcyc p hp

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