instCoeFunConnectedForallForallReachableElemVertsCoe

English

If H is connected, then for all u,v in H.verts, u is reachable from v within H.

Русский

Если H связен, то для любых вершин u,v из V(H) существует путь внутри H между ними.

LaTeX

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

Lean4

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

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