singletonSubgraph_fst_le_subgraphOfAdj

English

If u is adjacent to some v in G, then the singletonSubgraph at u is below the subgraphOfAdj hvw.

Русский

Если u смежна с другим узлом в G, то подграф-одиночка на u лежит ниже подграфа по hvw.

LaTeX

$$$\\text{singletonSubgraph}(u) \\le G.\\mathrm{subgraphOfAdj}(hvw)$$$

Lean4

theorem singletonSubgraph_fst_le_subgraphOfAdj {u v : V} {h : G.Adj u v} : G.singletonSubgraph u ≤ G.subgraphOfAdj h :=
  by simp

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