nonempty_subgraphOfAdj_verts — Mathlib

English

If v is adjacent to w in G, then the subgraph of G on hvw has at least one vertex; in fact it contains v.

Русский

Если v смежна с w в G, то подграф G.subgraphOfAdj hvw непуст; на самом деле в нем содержится вершина v.

LaTeX

$$$\\exists x\\, x \\in (G.subgraphOfAdj hvw).verts$$$

Lean4

instance nonempty_subgraphOfAdj_verts {v w : V} (hvw : G.Adj v w) : Nonempty (G.subgraphOfAdj hvw).verts :=
  ⟨⟨v, by simp⟩⟩

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