instCoeFunPreconnectedForallForallReachableElemVertsCoe

English

For any subgraph H of G, if H is preconnected, then for all u,v in H.verts, u is reachable from v within H.

Русский

Для любого подграфа H графа G, если H предсоединённый, то для любых вершин u,v из V(H) выполняется достижимость u от v внутри H.

LaTeX

$$$\forall H : G{\text Subgraph},\ H.\textPreconnected \Rightarrow \forall u,v \in H.verts,\ H.coe.Reachable(u,v).$$$

Lean4

instance {H : G.Subgraph} : CoeFun H.Preconnected (fun _ => ∀ u v : H.verts, H.coe.Reachable u v) :=
  ⟨fun h => h.coe⟩

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